1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro
5 -/
6 import data.set.lattice data.set.finite
src └──────────────┘ └─────────────┘
7 import topology.instances.ennreal
src └────────────────────────┘
8 measure_theory.outer_measure
src └──────────────────────────┘
9
10 /-!
11 # Measure spaces
12
13 Measures are restricted to a measurable space (associated by the type class `measurable_space`).
14 This allows us to prove equalities between measures by restricting to a generating set of the
15 measurable space.
16
17 On the other hand, the `μ.measure s` projection (i.e. the measure of `s` on the measure space `μ`)
18 is the _outer_ measure generated by `μ`. This gives us a unrestricted monotonicity rule and it is
19 somehow well-behaved on non-measurable sets.
20
21 This allows us for the `lebesgue` measure space to have the `borel` measurable space, but still be
22 a complete measure.
23 -/
24
25 noncomputable theory
26
27 open classical set lattice filter finset function
28 open_locale classical topological_space
29
30 universes u v w x
31
32 namespace measure_theory
33
34 section of_measurable
35 parameters {α : Type*} [measurable_space α]
id └──────────────┘
src └──────────────┘
typ └──────────────┘
36 parameters (m : Π (s : set α), is_measurable s → ennreal)
id └─┘ └───────────┘ ┴ └─────┘
src └─┘ └───────────┘ └─────┘
typ └─┘ └───────────┘ ┴ └─────┘
doc └───────────┘ └─────┘
37 parameters (m0 : m ∅ is_measurable.empty = 0)
id ┴ └─────────────────┘ ┴
src ┴ └─────────────────┘ ┴
typ ┴ └─────────────────┘ ┴
38 include m0
39
40 /-- Measure projection which is ∞ for non-measurable sets.
41
42 `measure'` is mainly used to derive the outer measure, for the main `measure` projection. -/
43 def measure' (s : set α) : ennreal := ⨅ h : is_measurable s, m s h
id └─┘ ┴ └─────┘ ┴ └───────────┘ ┴┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴ └───────────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └───────────┘ ┴┴ ┴ ┴ ┴
doc └─────┘ ┴ └───────────┘ ┴
44
45 lemma measure'_eq {s} (h : is_measurable s) : measure' s = m s h :=
id └───────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └──────┘ ┴
typ └───────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘ └──────┘
46 by simp [measure', h]
id └──────┘ ┴
src └────┘└──────┘└┘ └─
typ └────┘└──────┘└┘┴└─
doc └────┘└──────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────
47
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
48 lemma measure'_empty : measure' ∅ = 0 :=
id └──────┘ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴
doc └──────┘
49 (measure'_eq is_measurable.empty).trans m0
id └─────────┘ └─────────────────┘ └───┘ └┘
src └─────────┘ └─────────────────┘ └───┘
typ └─────────┘ └─────────────────┘ └───┘ └┘
50
51 lemma measure'_Union_nat
52 {f : ℕ → set α}
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
53 (hm : ∀i, is_measurable (f i))
id ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ └───────────┘ ┴ ┴
doc └───────────┘
54 (mU : m (⋃i, f i) (is_measurable.Union hm) = (∑i, m (f i) (hm i))) :
id ┴ ┴┴┴ ┴ ┴ └─────────────────┘ └┘ ┴ ┴┴┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ └─────────────────┘ └┘ ┴ ┴┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ ┴ ┴ ┴
55 measure' (⋃i, f i) = (∑i, measure' (f i)) :=
id └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘
56 (measure'_eq _).trans $ mU.trans $
id └─────────┘ └───┘ └┘└────┘
src └─────────┘ └───┘ └────┘
typ └─────────┘ └───┘ └┘└────┘
57 by congr; funext i; rw measure'_eq
id └─────────┘
src └───┘ └──────┘ └─┘└─────────┘└
typ └───┘ └──────┘ └─┘└─────────┘└
doc └──────┘ └─┘ └
txt └───┘ └──────┘ └─┘ └
par └───┘ └──────┘ └─┘ └
pid └┘ ┴ └
st └───────────────────┘└─────────┘└
58
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
59 /-- outer measure of a measure -/
60 def outer_measure' : outer_measure α :=
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
61 outer_measure.of_function measure' measure'_empty
id └───────────────────────┘ └──────┘ └────────────┘
src └───────────────────────┘ └──────┘ └────────────┘
typ └───────────────────────┘ └──────┘ └────────────┘
doc └───────────────────────┘ └──────┘
62
63 lemma measure'_Union_le_tsum_nat'
64 (mU : ∀ {f : ℕ → set α} (hm : ∀i, is_measurable (f i)),
id ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src ┴ └─┘ └───────────┘
typ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
65 m (⋃i, f i) (is_measurable.Union hm) ≤ (∑i, m (f i) (hm i)))
id ┴ ┴┴┴ ┴ ┴ └─────────────────┘ └┘ ┴ ┴┴┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ └─────────────────┘ └┘ ┴ ┴┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ ┴ ┴ ┴
66 (s : ℕ → set α) :
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
67 measure' (⋃i, s i) ≤ (∑i, measure' (s i)) :=
id └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘
68 begin
st └─────
69 by_cases h : ∀i, is_measurable (s i),
id └───────────┘ ┴
src └───────┘ └─┘ ┴ ┴└───────────┘┴ ┴ ┴
typ └───────┘ └─┘ ┴ ┴└───────────┘┴ ┴┴ ┴
doc └───────┘ └─┘ ┴ ┴└───────────┘┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
70 { rw [measure'_eq _ _ (is_measurable.Union h),
id └─────────┘ └─────────────────┘ ┴
src └──┘└─────────┘└───┘ └─────────────────┘┴ └──
typ └──┘└─────────┘└───┘ └─────────────────┘┴┴└──
doc └──┘ └───┘ ┴ └──
txt └──┘ └───┘ ┴ └──
par └──┘ └───┘ ┴ └──
pid └┘ └───┘ ┴ └──
st ───┘└─────────────────────────────────────────┘└─
71 congr_arg tsum _], {apply mU h},
id └───────┘ └──┘ └┘ ┴
src ───────┘└───────┘┴└──┘└─┘ └────┘ ┴
typ ───────┘└───────┘┴└──┘└─┘ └────┘└┘┴┴
doc ───────┘ ┴└──┘└─┘ └────┘ ┴
txt ───────┘ ┴ └─┘ └────┘ ┴
par ───────┘ ┴ └─┘ └────┘ ┴
pid ───────┘ ┴ └─┘ ┴ ┴
st ───────────────────────┘└────────────┘└┘└
72 funext i, apply measure'_eq _ _ (h i) },
id └─────────┘ ┴ ┴
src └──────┘ └────┘└─────────┘└───┘ ┴ └┘
typ └──────┘ └────┘└─────────┘└───┘ ┴┴┴└┘
doc └──────┘ └────┘ └───┘ ┴ └┘
txt └──────┘ └────┘ └───┘ ┴ └┘
par └──────┘ └────┘ └───┘ ┴ └┘
pid └┘ ┴ └───┘ ┴ ┴┴
st ───────────┘└────────────────────────────┘└┘└
73 { cases not_forall.1 h with i hi,
id └────────┘ ┴
src └────┘└────────┘└─┘ └────────┘
typ └────┘└────────┘└─┘┴└────────┘
doc └────┘ └─┘ └────────┘
txt └────┘ └─┘ └────────┘
par └────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ─────────────────────────────────┘└─
74 exact le_trans (le_infi $ λ h, hi.elim h) (ennreal.le_tsum i) }
id └──────┘ └─────┘ └─────┘ └─────────────┘ ┴
src └────┘└──────┘┴ └─────┘┴ ┴ └──┘└─────┘┴ └┘ └─────────────┘┴ └┘
typ └────┘└──────┘┴ └─────┘┴ ┴ └──┘└─────┘┴ └┘ └─────────────┘┴┴└┘
doc └────┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └┘
txt └────┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └┘
par └────┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └┘
pid ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────┘└─
75 end
st ──┘
76
77 parameter (mU : ∀ {f : ℕ → set α} (hm : ∀i, is_measurable (f i)),
id ┴ ┴ └─┘ ┴ └───────────┘ ┴ ┴
src ┴ └─┘ └───────────┘
typ ┴ ┴ └─┘ ┴ └───────────┘ ┴ ┴
doc └───────────┘
78 pairwise (disjoint on f) →
id └──────┘ └──────┘ └┘ ┴
src └──────┘ └──────┘ └┘
typ └──────┘ └──────┘ └┘ ┴
doc └──────┘ └──────┘
79 m (⋃i, f i) (is_measurable.Union hm) = (∑i, m (f i) (hm i)))
id ┴┴┴ ┴ ┴ └─────────────────┘ └┘ ┴ ┴┴┴ ┴ ┴ └┘ ┴
src ┴ ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ └─────────────────┘ └┘ ┴ ┴┴┴ ┴ ┴ └┘ ┴
doc ┴ ┴ ┴ ┴
80 include mU
81
82 lemma measure'_Union
83 {β} [encodable β] {f : β → set α}
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
84 (hd : pairwise (disjoint on f)) (hm : ∀i, is_measurable (f i)) :
id └──────┘ └──────┘ └┘ ┴ ┴ └───────────┘ ┴ ┴
src └──────┘ └──────┘ └┘ └───────────┘
typ └──────┘ └──────┘ └┘ ┴ ┴ └───────────┘ ┴ ┴
doc └──────┘ └──────┘ └───────────┘
85 measure' (⋃i, f i) = (∑i, measure' (f i)) :=
id └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘
86 begin
st └─────
87 rw [encodable.Union_decode2, outer_measure.Union_aux],
id └─────────────────────┘ └─────────────────────┘
src └──┘└─────────────────────┘└┘└─────────────────────┘┴
typ └──┘└─────────────────────┘└┘└─────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────────┘└───────────────────────┘└──
88 { exact measure'_Union_nat _ _
id └────────────────┘
src └────┘└────────────────┘└────
typ └────┘└────────────────┘└────
doc └────┘ └────
txt └────┘ └────
par └────┘ └────
pid ┴ └────
st ───┘└────────────────────────────
89 (λ n, encodable.Union_decode2_cases is_measurable.empty hm)
id └───────────────────────────┘ └─────────────────┘ └┘
src ─────┘ └──┘└───────────────────────────┘┴└─────────────────┘┴ └─
typ ─────┘ └──┘└───────────────────────────┘┴└─────────────────┘┴└┘└─
doc ─────┘ └──┘ ┴ ┴ └─
txt ─────┘ └──┘ ┴ ┴ └─
par ─────┘ └──┘ ┴ ┴ └─
pid ─────┘ └──┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────
90 (mU _ (measurable_space.Union_decode2_disjoint_on hd)) },
id └┘ └────────────────────────────────────────┘ └┘
src ─────┘ └─┘ └────────────────────────────────────────┘┴ └─┘
typ ─────┘ └┘└─┘ └────────────────────────────────────────┘┴└┘└─┘
doc ─────┘ └─┘ ┴ └─┘
txt ─────┘ └─┘ ┴ └─┘
par ─────┘ └─┘ ┴ └─┘
pid ─────┘ └─┘ ┴ └┘┴
st ────────────────────────────────────────────────────────────┘└┘└
91 { apply measure'_empty },
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────┘└──
92 end
st ──┘
93
94 lemma measure'_union {s₁ s₂ : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
95 (hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
id └──────┘ └┘ └┘ └───────────┘ └┘ └───────────┘ └┘
src └──────┘ └───────────┘ └───────────┘
typ └──────┘ └┘ └┘ └───────────┘ └┘ └───────────┘ └┘
doc └──────┘ └───────────┘ └───────────┘
96 measure' (s₁ ∪ s₂) = measure' s₁ + measure' s₂ :=
id └──────┘ └┘ ┴ └┘ ┴ └──────┘ └┘ ┴ └──────┘ └┘
src └──────┘ ┴ ┴ └──────┘ ┴ └──────┘
typ └──────┘ └┘ ┴ └┘ ┴ └──────┘ └┘ ┴ └──────┘ └┘
doc └──────┘ └──────┘ └──────┘
97 begin
st └─────
98 rw [union_eq_Union, measure'_Union _ _ @mU
id └────────────┘ └────────────┘ └┘
src └──┘└────────────┘└┘└────────────┘└───┘ └
typ └──┘└────────────┘└┘└────────────┘└───┘ └┘└
doc └──┘ └┘ └───┘ └
txt └──┘ └┘ └───┘ └
par └──┘ └┘ └───┘ └
pid └┘ └┘ └───┘ └
st ───────────────────┘└────────────────────────
99 (pairwise_disjoint_on_bool.2 hd) (bool.forall_bool.2 ⟨h₂, h₁⟩),
id └───────────────────────┘ └┘ └──────────────┘ └┘ └┘
src ─────┘ └───────────────────────┘└─┘ └┘ └──────────────┘└─┘ └┘ └───
typ ─────┘ └───────────────────────┘└─┘└┘└┘ └──────────────┘└─┘ └┘└┘└┘└───
doc ─────┘ └─┘ └┘ └─┘ └┘ └───
txt ─────┘ └─┘ └┘ └─┘ └┘ └───
par ─────┘ └─┘ └┘ └─┘ └┘ └───
pid ─────┘ └─┘ └┘ └─┘ └┘ └───
st ───────────────────────────────────────────────────────────────────┘└─
100 tsum_fintype],
id └──────────┘
src ───┘└──────────┘┴
typ ───┘└──────────┘┴
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ───────────────┘└──
101 change _+_ = _, simp
id ┴ ┴
src └──────┘┴└┘┴└┘ └───┘
typ └──────┘┴└┘┴└┘ └───┘
doc └──────┘ └┘ └┘ └───┘
txt └──────┘ └┘ └┘ └───┘
par └──────┘ └┘ └┘ └───┘
pid └┘ └┘ └┘ ┴
st ───────────────┘└─────┘
102 end
st └─┘
103
104 lemma measure'_mono {s₁ s₂ : set α} (h₁ : is_measurable s₁) (hs : s₁ ⊆ s₂) :
id └─┘ ┴ └───────────┘ └┘ └┘ ┴ └┘
src └─┘ └───────────┘ ┴
typ └─┘ ┴ └───────────┘ └┘ └┘ ┴ └┘
doc └───────────┘
105 measure' s₁ ≤ measure' s₂ :=
id └──────┘ └┘ ┴ └──────┘ └┘
src └──────┘ ┴ └──────┘
typ └──────┘ └┘ ┴ └──────┘ └┘
doc └──────┘ └──────┘
106 le_infi $ λ h₂, begin
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
st └─────
107 have := measure'_union _ _ @mU disjoint_diff h₁ (h₂.diff h₁),
id └────────────┘ └┘ └───────────┘ └─────┘ └┘
src └──────┘└────────────┘└───┘ ┴└───────────┘┴ ┴ └─────┘┴ ┴
typ └──────┘└────────────┘└───┘ └┘┴└───────────┘┴ ┴ └─────┘┴└┘┴
doc └──────┘ └───┘ ┴ ┴ ┴ ┴ ┴
txt └──────┘ └───┘ ┴ ┴ ┴ ┴ ┴
par └──────┘ └───┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
108 rw union_diff_cancel hs at this,
id └───────────────┘ └┘
src └─┘└───────────────┘┴ └──────┘
typ └─┘└───────────────┘┴└┘└──────┘
doc └─┘ ┴ └──────┘
txt └─┘ ┴ └──────┘
par └─┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ────────────────────────────────┘└─
109 rw ← measure'_eq m m0 _,
id └─────────┘ ┴ └┘
src └───┘└─────────┘┴ ┴ └┘
typ └───┘└─────────┘┴┴┴└┘└┘
doc └───┘ ┴ ┴ └┘
txt └───┘ ┴ ┴ └┘
par └───┘ ┴ ┴ └┘
pid └─┘ ┴ ┴ └┘
st ────────────────────────┘└─
110 exact le_iff_exists_add.2 ⟨_, this⟩
id └───────────────┘ └──┘
src └────┘└───────────────┘└─┘ └─┘ └┘
typ └────┘└───────────────┘└─┘ └─┘└──┘└┘
doc └────┘ └─┘ └─┘ └┘
txt └────┘ └─┘ └─┘ └┘
par └────┘ └─┘ └─┘ └┘
pid ┴ └─┘ └─┘ ┴┴
st ─────────────────────────────────────┘
111 end
st └─┘
112
113 lemma measure'_Union_le_tsum_nat : ∀ (s : ℕ → set α),
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
114 measure' (⋃i, s i) ≤ (∑i, measure' (s i)) :=
id └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘
115 measure'_Union_le_tsum_nat' $ λ f h, begin
id └─────────────────────────┘ ┴ ┴
src └─────────────────────────┘
typ └─────────────────────────┘ ┴ ┴
st └─────
116 simp [Union_disjointed.symm] {single_pass := tt},
id └┘
src └────┘ └┘ └─────────────┘└┘┴
typ └────┘└───────────────────┘└┘ └─────────────┘└┘┴
doc └────┘ └┘ └─────────────┘ ┴
txt └────┘ └┘ └─────────────┘ ┴
par └────┘ └┘ └─────────────┘ ┴
pid ┴┴ ┴┴ └─────────────┘ ┴
st ─────────────────────────────────────────────────┘└─
117 rw [mU (is_measurable.disjointed h) disjoint_disjointed],
id └┘ └──────────────────────┘ ┴ └─────────────────┘
src └──┘ ┴ └──────────────────────┘┴ └┘└─────────────────┘┴
typ └──┘└┘┴ └──────────────────────┘┴┴└┘└─────────────────┘┴
doc └──┘ ┴ ┴ └┘ ┴
txt └──┘ ┴ ┴ └┘ ┴
par └──┘ ┴ ┴ └┘ ┴
pid └┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────┘└──
118 refine ennreal.tsum_le_tsum (λ i, _),
id └──────────────────┘
src └─────┘└──────────────────┘┴ └────┘
typ └─────┘└──────────────────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ─────────────────────────────────────┘└─
119 rw [← measure'_eq m m0, ← measure'_eq m m0],
id └─────────┘ ┴ └┘ └─────────┘ ┴ └┘
src └────┘└─────────┘┴ ┴ └──┘└─────────┘┴ ┴ ┴
typ └────┘└─────────┘┴┴┴└┘└──┘└─────────┘┴┴┴└┘┴
doc └────┘ ┴ ┴ └──┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ └──┘ ┴ ┴ ┴
par └────┘ ┴ ┴ └──┘ ┴ ┴ ┴
pid └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
st ───────────────────────┘└──────────────────┘└──
120 exact measure'_mono _ _ @mU (is_measurable.disjointed h _) (inter_subset_left _ _)
id └───────────┘ └┘ └──────────────────────┘ ┴ └───────────────┘
src └────┘└───────────┘└───┘ ┴ └──────────────────────┘┴ └──┘ └───────────────┘└────┘
typ └────┘└───────────┘└───┘ └┘┴ └──────────────────────┘┴┴└──┘ └───────────────┘└────┘
doc └────┘ └───┘ ┴ ┴ └──┘ └────┘
txt └────┘ └───┘ ┴ ┴ └──┘ └────┘
par └────┘ └───┘ ┴ ┴ └──┘ └────┘
pid ┴ └───┘ ┴ ┴ └──┘ └───┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘
121 end
st └─┘
122
123 lemma outer_measure'_eq {s : set α} (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
124 outer_measure' s = m s hs :=
id └────────────┘ ┴ ┴ ┴ ┴ └┘
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴ └┘
doc └────────────┘
125 by rw ← measure'_eq m m0 hs; exact
id └─────────┘ ┴ └┘ └┘
src └───┘└─────────┘┴ ┴ ┴ └────┘
typ └───┘└─────────┘┴┴┴└┘┴└┘ └────┘
doc └───┘ ┴ ┴ ┴ └────┘
txt └───┘ ┴ ┴ ┴ └────┘
par └───┘ ┴ ┴ ┴ └────┘
pid └─┘ ┴ ┴ ┴ ┴
st └────────────────────────────────
126 (le_antisymm (outer_measure.of_function_le _ _ _) $
id └─────────┘ └──────────────────────────┘
src └─────────┘┴ └──────────────────────────┘└──────┘ └
typ └─────────┘┴ └──────────────────────────┘└──────┘ └
doc ┴ └──────┘ └
txt ┴ └──────┘ └
par ┴ └──────┘ └
pid ┴ └──────┘ └
st ────────────────────────────────────────────────────
127 le_infi $ λ f, le_infi $ λ hf,
id └─────┘
src ─┘ ┴ ┴ └──┘└─────┘┴ ┴ └────
typ ─┘ ┴ ┴ └──┘└─────┘┴ ┴ └────
doc ─┘ ┴ ┴ └──┘ ┴ ┴ └────
txt ─┘ ┴ ┴ └──┘ ┴ ┴ └────
par ─┘ ┴ ┴ └──┘ ┴ ┴ └────
pid ─┘ ┴ ┴ └──┘ ┴ ┴ └────
st ─────────────────────────────────
128 le_trans (measure'_mono _ _ @mU hs hf) $
id └──────┘ └───────────┘ └┘ └┘
src ─┘└──────┘┴ └───────────┘└───┘ ┴ ┴ └┘ └
typ ─┘└──────┘┴ └───────────┘└───┘ └┘┴└┘┴ └┘ └
doc ─┘ ┴ └───┘ ┴ ┴ └┘ └
txt ─┘ ┴ └───┘ ┴ ┴ └┘ └
par ─┘ ┴ └───┘ ┴ ┴ └┘ └
pid ─┘ ┴ └───┘ ┴ ┴ └┘ └
st ───────────────────────────────────────────
129 measure'_Union_le_tsum_nat _ _ @mU _)
id └────────────────────────┘ └┘
src ─┘└────────────────────────┘└───┘ └───
typ ─┘└────────────────────────┘└───┘ └┘└───
doc ─┘ └───┘ └───
txt ─┘ └───┘ └───
par ─┘ └───┘ └───
pid ─┘ └───┘ └─┘└
st ────────────────────────────────────────
130
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
131 lemma outer_measure'_eq_measure' {s : set α} (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
132 outer_measure' s = measure' s :=
id └────────────┘ ┴ ┴ └──────┘ ┴
src └────────────┘ ┴ └──────┘
typ └────────────┘ ┴ ┴ └──────┘ ┴
doc └────────────┘ └──────┘
133 by rw [measure'_eq m m0 hs, outer_measure'_eq m m0 @mU hs]
id └─────────┘ ┴ └┘ └┘ └───────────────┘ ┴ └┘ └┘ └┘
src └──┘└─────────┘┴ ┴ ┴ └┘└───────────────┘┴ ┴ ┴ ┴ └─
typ └──┘└─────────┘┴┴┴└┘┴└┘└┘└───────────────┘┴┴┴└┘┴ └┘┴└┘└─
doc └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
txt └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
par └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
pid └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴└
st └──────────────────────┘└─────────────────────────────┘┴└
134
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
135 end of_measurable
136
137 namespace outer_measure
138 variables {α : Type*} [measurable_space α] (m : outer_measure α)
id ┴ └──────────────┘ └───────────┘
src └──────────────┘ └───────────┘
typ ┴ └──────────────┘ └───────────┘
139
140 def trim : outer_measure α :=
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
141 outer_measure' (λ s _, m s) m.empty
id └────────────┘ ┴ ┴ ┴ ┴ ┴└────┘
src └────────────┘ └────┘
typ └────────────┘ ┴ ┴ ┴ ┴ ┴└────┘
doc └────────────┘
142
143 theorem trim_ge : m ≤ m.trim :=
id ┴ ┴ ┴└───┘
src ┴ └───┘
typ ┴ ┴ ┴└───┘
144 λ s, le_infi $ λ f, le_infi $ λ hs,
id ┴ └─────┘ ┴ └─────┘ └┘
src └─────┘ └─────┘
typ ┴ └─────┘ ┴ └─────┘ └┘
145 le_trans (m.mono hs) $ le_trans (m.Union_nat f) $
id └──────┘ ┴└───┘ └┘ └──────┘ ┴└────────┘ ┴
src └──────┘ └───┘ └──────┘ └────────┘
typ └──────┘ ┴└───┘ └┘ └──────┘ ┴└────────┘ ┴
146 ennreal.tsum_le_tsum $ λ i, le_infi $ λ hf, le_refl _
id └──────────────────┘ ┴ └─────┘ └┘ └─────┘
src └──────────────────┘ └─────┘ └─────┘
typ └──────────────────┘ ┴ └─────┘ └┘ └─────┘
147
148 theorem trim_eq {s : set α} (hs : is_measurable s) : m.trim s = m s :=
id └─┘ ┴ └───────────┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
src └─┘ └───────────┘ └───┘ ┴
typ └─┘ ┴ └───────────┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴
doc └───────────┘
149 le_antisymm (le_trans (of_function_le _ _ _) (infi_le _ hs)) (trim_ge _ _)
id └─────────┘ └──────┘ └────────────┘ └─────┘ └┘ └─────┘
src └─────────┘ └──────┘ └────────────┘ └─────┘ └─────┘
typ └─────────┘ └──────┘ └────────────┘ └─────┘ └┘ └─────┘
150
151 theorem trim_congr {m₁ m₂ : outer_measure α}
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
152 (H : ∀ {s : set α}, is_measurable s → m₁ s = m₂ s) :
id └─┘ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ └───────────┘ ┴
typ └─┘ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴
doc └───────────┘
153 m₁.trim = m₂.trim :=
id └┘└───┘ ┴ └┘└───┘
src └───┘ ┴ └───┘
typ └┘└───┘ ┴ └┘└───┘
154 by unfold trim; congr; funext s hs; exact H hs
id ┴ └┘
src └─────────┘ └───┘ └─────────┘ └────┘ ┴ └
typ └─────────┘ └───┘ └─────────┘ └────┘┴┴└┘└
doc └─────────┘ └─────────┘ └────┘ ┴ └
txt └─────────┘ └───┘ └─────────┘ └────┘ ┴ └
par └─────────┘ └───┘ └─────────┘ └────┘ ┴ └
pid └───┘ └───┘ ┴ ┴ └
st └────────────────────────────────────────────
155
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
156 theorem trim_le_trim {m₁ m₂ : outer_measure α} (H : m₁ ≤ m₂) : m₁.trim ≤ m₂.trim :=
id └───────────┘ ┴ └┘ ┴ └┘ └┘└───┘ ┴ └┘└───┘
src └───────────┘ ┴ └───┘ ┴ └───┘
typ └───────────┘ ┴ └┘ ┴ └┘ └┘└───┘ ┴ └┘└───┘
157 λ s, infi_le_infi $ λ f, infi_le_infi $ λ hs,
id ┴ └──────────┘ ┴ └──────────┘ └┘
src └──────────┘ └──────────┘
typ ┴ └──────────┘ ┴ └──────────┘ └┘
158 ennreal.tsum_le_tsum $ λ b, infi_le_infi $ λ hf, H _
id └──────────────────┘ ┴ └──────────┘ └┘ ┴
src └──────────────────┘ └──────────┘
typ └──────────────────┘ ┴ └──────────┘ └┘ ┴
159
160 theorem le_trim_iff {m₁ m₂ : outer_measure α} : m₁ ≤ m₂.trim ↔
id └───────────┘ ┴ └┘ ┴ └┘└───┘ ┴
src └───────────┘ ┴ └───┘ ┴
typ └───────────┘ ┴ └┘ ┴ └┘└───┘ ┴
161 ∀ s, is_measurable s → m₁ s ≤ m₂ s :=
id ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src └───────────┘ ┴
typ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴
doc └───────────┘
162 le_of_function.trans $ forall_congr $ λ s, le_infi_iff
id └────────────┘└────┘ └──────────┘ ┴ └─────────┘
src └────────────┘└────┘ └──────────┘ └─────────┘
typ └────────────┘└────┘ └──────────┘ ┴ └─────────┘
163
164 theorem trim_eq_infi (s : set α) : m.trim s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), m t :=
id └─┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └─┘ └───┘ ┴ ┴ ┴ └───────────┘ ┴
typ └─┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc ┴ └───────────┘ ┴
165 begin
st └─────
166 refine le_antisymm
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────
167 (le_infi $ λ t, le_infi $ λ st, le_infi $ λ ht, _)
src ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └───────
typ ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └───────
doc ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └───────
txt ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └───────
par ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └───────
pid ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └───────
st ───────────────────────────────────────────────────────
168 (le_infi $ λ f, le_infi $ λ hf, _),
id └─────┘
src ───┘ ┴ ┴ └──┘└─────┘┴ ┴ └─────┘
typ ───┘ ┴ ┴ └──┘└─────┘┴ ┴ └─────┘
doc ───┘ ┴ ┴ └──┘ ┴ ┴ └─────┘
txt ───┘ ┴ ┴ └──┘ ┴ ┴ └─────┘
par ───┘ ┴ ┴ └──┘ ┴ ┴ └─────┘
pid ───┘ ┴ ┴ └──┘ ┴ ┴ └─────┘
st ─────────────────────────────────────┘└─
169 { rw ← trim_eq m ht, exact (trim m).mono st },
id └─────┘ ┴ └┘ └──┘ ┴ └┘
src └───┘└─────┘┴ ┴ └────┘ └──┘┴ └─────┘ ┴
typ └───┘└─────┘┴┴┴└┘ └────┘ └──┘┴┴└─────┘└┘┴
doc └───┘ ┴ ┴ └────┘ ┴ └─────┘ ┴
txt └───┘ ┴ ┴ └────┘ ┴ └─────┘ ┴
par └───┘ ┴ ┴ └────┘ ┴ └─────┘ ┴
pid └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴
st ───┘└───────────────┘└───────────────────────┘└┘└
170 { by_cases h : ∀i, is_measurable (f i),
id └───────────┘ ┴
src └───────┘ └─┘ ┴ ┴└───────────┘┴ ┴ ┴
typ └───────┘ └─┘ ┴ ┴└───────────┘┴ ┴┴ ┴
doc └───────┘ └─┘ ┴ ┴└───────────┘┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
171 { refine infi_le_of_le _ (infi_le_of_le hf $
id └┘
src └─────┘ └─┘ ┴ ┴ └
typ └─────┘ └─┘ ┴└┘┴ └
doc └─────┘ └─┘ ┴ ┴ └
txt └─────┘ └─┘ ┴ ┴ └
par └─────┘ └─┘ ┴ ┴ └
pid ┴ └─┘ ┴ ┴ └
st ─────┘└──────────────────────────────────────────
172 infi_le_of_le (is_measurable.Union h) _),
id └───────────┘ └─────────────────┘ ┴
src ───────┘└───────────┘┴ └─────────────────┘┴ └──┘
typ ───────┘└───────────┘┴ └─────────────────┘┴┴└──┘
doc ───────┘ ┴ ┴ └──┘
txt ───────┘ ┴ ┴ └──┘
par ───────┘ ┴ ┴ └──┘
pid ───────┘ ┴ ┴ └──┘
st ───────────────────────────────────────────────┘└─
173 rw congr_arg tsum _, {exact m.Union_nat _},
id └───────┘ └──┘ └─────────┘
src └─┘└───────┘┴└──┘└┘ └────┘└─────────┘└┘
typ └─┘└───────┘┴└──┘└┘ └────┘└─────────┘└┘
doc └─┘ ┴└──┘└┘ └────┘ └┘
txt └─┘ ┴ └┘ └────┘ └┘
par └─┘ ┴ └┘ └────┘ └┘
pid ┴ ┴ └┘ ┴ └┘
st ────────────────────────┘└────────────────────┘└┘└
174 funext i, exact measure'_eq _ _ (h i) },
id └─────────┘ ┴ ┴
src └──────┘ └────┘└─────────┘└───┘ ┴ └┘
typ └──────┘ └────┘└─────────┘└───┘ ┴┴┴└┘
doc └──────┘ └────┘ └───┘ ┴ └┘
txt └──────┘ └────┘ └───┘ ┴ └┘
par └──────┘ └────┘ └───┘ ┴ └┘
pid └┘ ┴ └───┘ ┴ ┴┴
st ─────────────┘└────────────────────────────┘└┘└
175 { cases not_forall.1 h with i hi,
id └────────┘ ┴
src └────┘└────────┘└─┘ └────────┘
typ └────┘└────────┘└─┘┴└────────┘
doc └────┘ └─┘ └────────┘
txt └────┘ └─┘ └────────┘
par └────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ───────────────────────────────────┘└─
176 exact le_trans (le_infi $ λ h, hi.elim h) (ennreal.le_tsum i) } }
id └──────┘ └─────┘ └─────┘ └─────────────┘ ┴
src └────┘└──────┘┴ └─────┘┴ ┴ └──┘└─────┘┴ └┘ └─────────────┘┴ └┘
typ └────┘└──────┘┴ └─────┘┴ ┴ └──┘└─────┘┴ └┘ └─────────────┘┴┴└┘
doc └────┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └┘
txt └────┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └┘
par └────┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └┘
pid ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴┴
st ───────────────────────────────────────────────────────────────────┘└───
177 end
st ──┘
178
179 theorem trim_eq_infi' (s : set α) : m.trim s = ⨅ t : {t // s ⊆ t ∧ is_measurable t}, m t.1 :=
id └─┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴
src └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
typ └─┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴
doc ┴ └───────────┘ ┴
180 by simp [infi_subtype, infi_and, trim_eq_infi]
id └──────────┘ └──────┘ └──────────┘
src └────┘└──────────┘└┘└──────┘└┘└──────────┘└─
typ └────┘└──────────┘└┘└──────┘└┘└──────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └────────────────────────────────────────────
181
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
182 theorem trim_trim (m : outer_measure α) : m.trim.trim = m.trim :=
id └───────────┘ ┴ ┴└────────┘ ┴ ┴└───┘
src └───────────┘ └────────┘ ┴ └───┘
typ └───────────┘ ┴ ┴└────────┘ ┴ ┴└───┘
183 le_antisymm (le_trim_iff.2 $ λ s hs, by simp [trim_eq _ hs, le_refl]) (trim_ge _)
id └─────────┘ └─────────┘┴ ┴ └┘ └─────┘ └┘ └─────┘ └─────┘
src └─────────┘ └─────────┘┴ └────┘└─────┘└─┘ └┘└─────┘┴ └─────┘
typ └─────────┘ └─────────┘┴ ┴ └┘ └────┘└─────┘└─┘└┘└┘└─────┘┴ └─────┘
doc └────┘ └─┘ └┘ ┴
txt └────┘ └─┘ └┘ ┴
par └────┘ └─┘ └┘ ┴
pid ┴┴ └─┘ └┘ ┴
st └───────────────────────────┘
184
185 theorem trim_zero : (0 : outer_measure α).trim = 0 :=
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘ ┴
typ └───────────┘ ┴ └──┘ ┴
186 ext $ λ s, le_antisymm
id └─┘ ┴ └─────────┘
src └─┘ └─────────┘
typ └─┘ ┴ └─────────┘
187 (le_trans ((trim 0).mono (subset_univ s)) $
id └──────┘ └──┘ └──┘ └─────────┘ ┴
src └──────┘ └──┘ └──┘ └─────────┘
typ └──────┘ └──┘ └──┘ └─────────┘ ┴
188 le_of_eq $ trim_eq _ is_measurable.univ)
id └──────┘ └─────┘ └────────────────┘
src └──────┘ └─────┘ └────────────────┘
typ └──────┘ └─────┘ └────────────────┘
189 (zero_le _)
id └─────┘
src └─────┘
typ └─────┘
190
191 theorem trim_add (m₁ m₂ : outer_measure α) : (m₁ + m₂).trim = m₁.trim + m₂.trim :=
id └───────────┘ ┴ └┘ ┴ └┘ └──┘ ┴ └┘└───┘ ┴ └┘└───┘
src └───────────┘ ┴ └──┘ ┴ └───┘ ┴ └───┘
typ └───────────┘ ┴ └┘ ┴ └┘ └──┘ ┴ └┘└───┘ ┴ └┘└───┘
192 ext $ λ s, begin
id └─┘ ┴
src └─┘
typ └─┘ ┴
st └─────
193 simp [trim_eq_infi'],
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────────────┘└─
194 rw ennreal.infi_add_infi,
id └───────────────────┘
src └─┘└───────────────────┘
typ └─┘└───────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────┘└─
195 rintro ⟨t₁, st₁, ht₁⟩ ⟨t₂, st₂, ht₂⟩,
src └──────────────────────────────────┘
typ └──────────────────────────────────┘
doc └──────────────────────────────────┘
txt └──────────────────────────────────┘
par └──────────────────────────────────┘
pid └────────────────────────────┘
st ─────────────────────────────────────┘└─
196 exact ⟨⟨_, subset_inter_iff.2 ⟨st₁, st₂⟩, ht₁.inter ht₂⟩,
id └──────────────┘ └─┘ └─┘ └───────┘ └─┘
src └────┘ └─┘└──────────────┘└─┘ └┘ └─┘└───────┘┴ └──
typ └────┘ └─┘└──────────────┘└─┘ └─┘└┘└─┘└─┘└───────┘┴└─┘└──
doc └────┘ └─┘ └─┘ └┘ └─┘ ┴ └──
txt └────┘ └─┘ └─┘ └┘ └─┘ ┴ └──
par └────┘ └─┘ └─┘ └┘ └─┘ ┴ └──
pid ┴ └─┘ └─┘ └┘ └─┘ ┴ └──
st ────────────────────────────────────────────────────────────
197 add_le_add'
id └─────────┘
src ───┘└─────────┘└
typ ───┘└─────────┘└
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ────────────────
198 (m₁.mono' (inter_subset_left _ _))
id └──────┘ └───────────────┘
src ─────┘ └──────┘┴ └───────────────┘└──────
typ ─────┘ └──────┘┴ └───────────────┘└──────
doc ─────┘ ┴ └──────
txt ─────┘ ┴ └──────
par ─────┘ ┴ └──────
pid ─────┘ ┴ └──────
st ─────────────────────────────────────────
199 (m₂.mono' (inter_subset_right _ _))⟩,
id └──────┘ └────────────────┘
src ─────┘ └──────┘┴ └────────────────┘└─────┘
typ ─────┘ └──────┘┴ └────────────────┘└─────┘
doc ─────┘ ┴ └─────┘
txt ─────┘ ┴ └─────┘
par ─────┘ ┴ └─────┘
pid ─────┘ ┴ └─────┘
st ─────────────────────────────────────────┘└─
200 end
st ──┘
201
202 theorem trim_sum_ge {ι} (m : ι → outer_measure α) : sum (λ i, (m i).trim) ≤ (sum m).trim :=
id ┴ └───────────┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └──┘
src └───────────┘ └─┘ └──┘ ┴ └─┘ └──┘
typ ┴ └───────────┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └──┘
203 λ s, by simp [trim_eq_infi]; exact
id ┴ └──────────┘
src └────┘└──────────┘┴ └────┘
typ ┴ └────┘└──────────┘┴ └────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴┴ ┴ ┴
st └───────────────────────────
204 λ t st ht, ennreal.tsum_le_tsum (λ i,
id └──────────────────┘
src └────────┘└──────────────────┘┴ └───
typ └────────┘└──────────────────┘┴ └───
doc └────────┘ ┴ └───
txt └────────┘ ┴ └───
par └────────┘ ┴ └───
pid └────────┘ ┴ └───
st ──────────────────────────────────────
205 infi_le_of_le t $ infi_le_of_le st $ infi_le _ ht)
id └───────────┘ └─────┘
src ─┘ ┴ ┴ ┴└───────────┘┴ ┴ ┴└─────┘└─┘ └─
typ ─┘ ┴ ┴ ┴└───────────┘┴ ┴ ┴└─────┘└─┘ └─
doc ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└
st ─────────────────────────────────────────────────────
206
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
207 end outer_measure
208
209 structure measure (α : Type*) [measurable_space α] extends outer_measure α :=
id └───┘ └──────────────┘ ┴ └───────────┘ ┴
src └──────────────┘ └───────────┘
typ └───┘ └──────────────┘ ┴ └───────────┘ ┴
210 (m_Union {f : ℕ → set α} :
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
211 (∀i, is_measurable (f i)) → pairwise (disjoint on f) →
id ┴ └───────────┘ ┴ ┴ └──────┘ └──────┘ └┘ ┴
src └───────────┘ └──────┘ └──────┘ └┘
typ ┴ └───────────┘ ┴ ┴ └──────┘ └──────┘ └┘ ┴
doc └───────────┘ └──────┘ └──────┘
212 measure_of (⋃i, f i) = (∑i, measure_of (f i)))
id └────────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └────────┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └────────┘ ┴ ┴
doc ┴ ┴ ┴ ┴
213 (trimmed : to_outer_measure.trim = to_outer_measure)
id └──────────────┘└───┘ ┴ └──────────────┘
src └───┘ ┴
typ └──────────────┘└───┘ ┴ └──────────────┘
214
215 /-- Measure projections for a measure space.
216
217 For measurable sets this returns the measure assigned by the `measure_of` field in `measure`.
218 But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and
219 subadditivity for all sets.
220 -/
221 instance measure.has_coe_to_fun {α} [measurable_space α] : has_coe_to_fun (measure α) :=
id └──────────────┘ ┴ └────────────┘ └─────┘ ┴
src └──────────────┘ └────────────┘ └─────┘
typ └──────────────┘ ┴ └────────────┘ └─────┘ ┴
222 ⟨λ _, set α → ennreal, λ m, m.to_outer_measure⟩
id ┴ └─┘ ┴ └─────┘ ┴ ┴└───────────────┘
src └─┘ └─────┘ └───────────────┘
typ ┴ └─┘ ┴ └─────┘ ┴ ┴└───────────────┘
doc └─────┘
223
224 namespace measure
225
226 def of_measurable {α} [measurable_space α]
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
227 (m : Π (s : set α), is_measurable s → ennreal)
id └─┘ ┴ └───────────┘ ┴ └─────┘
src └─┘ └───────────┘ └─────┘
typ └─┘ ┴ └───────────┘ ┴ └─────┘
doc └───────────┘ └─────┘
228 (m0 : m ∅ is_measurable.empty = 0)
id ┴ ┴ └─────────────────┘ ┴
src ┴ └─────────────────┘ ┴
typ ┴ ┴ └─────────────────┘ ┴
229 (mU : ∀ {f : ℕ → set α} (h : ∀i, is_measurable (f i)),
id ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src ┴ └─┘ └───────────┘
typ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
230 pairwise (disjoint on f) →
id └──────┘ └──────┘ └┘ ┴
src └──────┘ └──────┘ └┘
typ └──────┘ └──────┘ └┘ ┴
doc └──────┘ └──────┘
231 m (⋃i, f i) (is_measurable.Union h) = (∑i, m (f i) (h i))) :
id ┴ ┴┴┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
232 measure α :=
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
233 { m_Union := λ f hf hd,
id ┴ └┘ └┘
typ ┴ └┘ └┘
234 show outer_measure' m m0 (Union f) =
id └────────────┘ ┴ └┘ └───┘ ┴ ┴
src └────────────┘ └───┘ ┴
typ └────────────┘ ┴ └┘ └───┘ ┴ ┴
doc └────────────┘ └───┘
235 ∑ i, outer_measure' m m0 (f i), begin
id ┴ ┴┴ └────────────┘ ┴ └┘ ┴ ┴
src ┴ ┴ └────────────┘
typ ┴ ┴┴ └────────────┘ ┴ └┘ ┴ ┴
doc ┴ ┴ └────────────┘
st └─────
236 rw [outer_measure'_eq m m0 @mU, mU hf hd],
id └───────────────┘ ┴ └┘ └┘ └┘ └┘ └┘
src └──┘└───────────────┘┴ ┴ ┴ └┘ ┴ ┴ ┴
typ └──┘└───────────────┘┴┴┴└┘┴ └┘└┘└┘┴└┘┴└┘┴
doc └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────┘└────────┘└──
237 congr, funext n, rw outer_measure'_eq m m0 @mU
id └───────────────┘ ┴ └┘ └┘
src └───┘ └──────┘ └─┘└───────────────┘┴ ┴ ┴ └
typ └───┘ └──────┘ └─┘└───────────────┘┴┴┴└┘┴ └┘└
doc └──────┘ └─┘ ┴ ┴ ┴ └
txt └───┘ └──────┘ └─┘ ┴ ┴ ┴ └
par └───┘ └──────┘ └─┘ ┴ ┴ ┴ └
pid └┘ ┴ ┴ ┴ ┴ └
st ────────┘└────────┘└───────────────────────────────
238 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
239 trimmed :=
240 show (outer_measure' m m0).trim = outer_measure' m m0, begin
id └────────────┘ ┴ └┘ └──┘ ┴ └────────────┘ ┴ └┘
src └────────────┘ └──┘ ┴ └────────────┘
typ └────────────┘ ┴ └┘ └──┘ ┴ └────────────┘ ┴ └┘
doc └────────────┘ └────────────┘
st └─────
241 unfold outer_measure.trim,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └─────────────────┘
st ────────────────────────────┘└─
242 congr, funext s hs,
src └───┘ └─────────┘
typ └───┘ └─────────┘
doc └─────────┘
txt └───┘ └─────────┘
par └───┘ └─────────┘
pid └───┘
st ────────┘└───────────┘└─
243 exact outer_measure'_eq m m0 @mU hs
id └───────────────┘ ┴ └┘ └┘ └┘
src └────┘└───────────────┘┴ ┴ ┴ ┴ └
typ └────┘└───────────────┘┴┴┴└┘┴ └┘┴└┘└
doc └────┘ ┴ ┴ ┴ ┴ └
txt └────┘ ┴ ┴ ┴ ┴ └
par └────┘ ┴ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ └
st ────────────────────────────────────────
244 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
245 ..outer_measure' m m0 }
id └────────────┘ ┴ └┘
src └────────────┘
typ └────────────┘ ┴ └┘
doc └────────────┘
246
247 lemma of_measurable_apply {α} [measurable_space α]
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
248 {m : Π (s : set α), is_measurable s → ennreal}
id └─┘ ┴ └───────────┘ ┴ └─────┘
src └─┘ └───────────┘ └─────┘
typ └─┘ ┴ └───────────┘ ┴ └─────┘
doc └───────────┘ └─────┘
249 {m0 : m ∅ is_measurable.empty = 0}
id ┴ ┴ └─────────────────┘ ┴
src ┴ └─────────────────┘ ┴
typ ┴ ┴ └─────────────────┘ ┴
250 {mU : ∀ {f : ℕ → set α} (h : ∀i, is_measurable (f i)),
id ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src ┴ └─┘ └───────────┘
typ ┴ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘
251 pairwise (disjoint on f) →
id └──────┘ └──────┘ └┘ ┴
src └──────┘ └──────┘ └┘
typ └──────┘ └──────┘ └┘ ┴
doc └──────┘ └──────┘
252 m (⋃i, f i) (is_measurable.Union h) = (∑i, m (f i) (h i))}
id ┴ ┴┴┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
253 (s : set α) (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
254 of_measurable m m0 @mU s = m s hs :=
id └───────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘
src └───────────┘ ┴
typ └───────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘
255 outer_measure'_eq m m0 @mU hs
id └───────────────┘ ┴ └┘ └┘ └┘
src └───────────────┘
typ └───────────────┘ ┴ └┘ └┘ └┘
256
257 @[ext] lemma ext {α} [measurable_space α] :
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
doc └─┘
258 ∀ {μ₁ μ₂ : measure α}, (∀s, is_measurable s → μ₁ s = μ₂ s) → μ₁ = μ₂
id ┴ └─────┘ ┴ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
src └─────┘ └───────────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
doc └───────────┘
259 | ⟨m₁, u₁, h₁⟩ ⟨m₂, u₂, h₂⟩ h := by congr; rw [← h₁, ← h₂];
id └┘ └┘
src └───┘ └────┘ └──┘ ┴
typ └───┘ └────┘└┘└──┘└┘┴
doc └────┘ └──┘ ┴
txt └───┘ └────┘ └──┘ ┴
par └───┘ └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st └──────────┘└──┘└────┘┴└─
260 exact outer_measure.trim_congr h
id └──────────────────────┘ ┴
src └────┘└──────────────────────┘┴ └
typ └────┘└──────────────────────┘┴┴└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ───────────────────────────────────
261
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
262 end measure
263
264 section
265 variables {α : Type*} {β : Type*} [measurable_space α] {μ μ₁ μ₂ : measure α} {s s₁ s₂ : set α}
id ┴ └──────────────┘ └─────┘ └─┘
src └──────────────┘ └─────┘ └─┘
typ ┴ └──────────────┘ └─────┘ └─┘
266
267 @[simp] lemma to_outer_measure_apply (s) : μ.to_outer_measure s = μ s := rfl
id ┴└───────────────┘ ┴ ┴ ┴ ┴ └─┘
src └───────────────┘ ┴ └─┘
typ ┴└───────────────┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘
268
269 lemma measure_eq_trim (s) : μ s = μ.to_outer_measure.trim s :=
id ┴ ┴ ┴ ┴└───────────────┘└───┘ ┴
src ┴ └───────────────┘└───┘
typ ┴ ┴ ┴ ┴└───────────────┘└───┘ ┴
270 by rw μ.trimmed; refl
src └─┘ └────
typ └─┘└───────┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────────────
271
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
272 lemma measure_eq_infi (s) : μ s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), μ t :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └───────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc ┴ └───────────┘ ┴
273 by rw [measure_eq_trim, outer_measure.trim_eq_infi]; refl
id └─────────────┘ └────────────────────────┘
src └──┘└─────────────┘└┘└────────────────────────┘┴ └────
typ └──┘└─────────────┘└┘└────────────────────────┘┴ └────
doc └──┘ └┘ ┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └
st └──────────────────┘└──────────────────────────┘┴└──────
274
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
275 lemma measure_eq_outer_measure' :
276 μ s = outer_measure' (λ s _, μ s) μ.empty s :=
id ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴
src ┴ └────────────┘ └────┘
typ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴
doc └────────────┘
277 measure_eq_trim _
id └─────────────┘
src └─────────────┘
typ └─────────────┘
278
279 lemma to_outer_measure_eq_outer_measure' :
280 μ.to_outer_measure = outer_measure' (λ s _, μ s) μ.empty :=
id ┴└───────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└────┘
src └───────────────┘ ┴ └────────────┘ └────┘
typ ┴└───────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└────┘
doc └────────────┘
281 μ.trimmed.symm
id ┴└──────┘└───┘
src └──────┘└───┘
typ ┴└──────┘└───┘
282
283 lemma measure_eq_measure' (hs : is_measurable s) :
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
284 μ s = measure' (λ s _, μ s) μ.empty s :=
id ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴
src ┴ └──────┘ └────┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴
doc └──────┘
285 by rw [measure_eq_outer_measure',
id └───────────────────────┘
src └──┘└───────────────────────┘└─
typ └──┘└───────────────────────┘└─
doc └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ └─
st └────────────────────────────┘└─
286 outer_measure'_eq_measure' (λ s _, μ s) _ μ.m_Union hs]
id └────────────────────────┘ └───────┘ └┘
src ─┘└────────────────────────┘┴ └────┘ ┴ └──┘└───────┘┴ └─
typ ─┘└────────────────────────┘┴ └────┘ ┴ └──┘└───────┘┴└┘└─
doc ─┘ ┴ └────┘ ┴ └──┘ ┴ └─
txt ─┘ ┴ └────┘ ┴ └──┘ ┴ └─
par ─┘ ┴ └────┘ ┴ └──┘ ┴ └─
pid ─┘ ┴ └────┘ ┴ └──┘ ┴ ┴└
st ───────────────────────────────────────────────────────┘┴└
287
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
288 @[simp] lemma measure_empty : μ ∅ = 0 := μ.empty
id ┴ ┴ ┴ ┴└────┘
src ┴ ┴ └────┘
typ ┴ ┴ ┴ ┴└────┘
doc └──┘
289
290 lemma measure_mono (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ := μ.mono h
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴└───┘ ┴
src ┴ ┴ └───┘
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴└───┘ ┴
291
292 lemma measure_mono_null (h : s₁ ⊆ s₂) (h₂ : μ s₂ = 0) : μ s₁ = 0 :=
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴
293 by rw [← le_zero_iff_eq, ← h₂]; exact measure_mono h
id └────────────┘ └┘ └──────────┘ ┴
src └────┘└────────────┘└──┘ ┴ └────┘└──────────┘┴ └
typ └────┘└────────────┘└──┘└┘┴ └────┘└──────────┘┴┴└
doc └────┘ └──┘ ┴ └────┘ ┴ └
txt └────┘ └──┘ ┴ └────┘ ┴ └
par └────┘ └──┘ ┴ └────┘ ┴ └
pid └──┘ └──┘ ┴ ┴ ┴ └
st └───────────────────┘└────┘┴└──────────────────────
294
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
295 lemma exists_is_measurable_superset_of_measure_eq_zero {s : set α} (h : μ s = 0) :
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴
296 ∃t, s ⊆ t ∧ is_measurable t ∧ μ t = 0 :=
id ┴┴┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
297 begin
st └─────
298 rw [measure_eq_infi] at h,
id └─────────────┘
src └──┘└─────────────┘└────┘
typ └──┘└─────────────┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid └┘ ┴└───┘
st ────────────────────┘┴└───┘└─
299 have h := (infi_eq_bot _).1 h,
id └─────────┘ ┴
src └────────┘ └─────────┘└────┘
typ └────────┘ └─────────┘└────┘┴
doc └────────┘ └────┘
txt └────────┘ └────┘
par └────────┘ └────┘
pid └────┘┴└─┘ └────┘
st ──────────────────────────────┘└─
300 choose t ht using show ∀n:ℕ, ∃t, s ⊆ t ∧ is_measurable t ∧ μ t < n⁻¹,
id ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └┘
src └────────────────┘ ┴ └┘ ┴┴┴┴┴ ┴┴┴ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴┴┴ └┘└─
typ └────────────────┘ ┴ └┘ ┴┴┴┴┴┴┴┴┴ ┴ ┴└───────────┘┴ ┴ ┴┴┴ ┴┴┴ └┘└─
doc └────────────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
txt └────────────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par └────────────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid └┘└─┘└─────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────────
301 { assume n,
src ───┘└──────┘└─
typ ───┘└──────┘└─
doc ───┘└──────┘└─
txt ───┘└──────┘└─
par ───┘└──────┘└─
pid ──────────────
st ──┘└───────┘└─
302 have : (0 : ennreal) < n⁻¹ :=
id └─────┘ ┴
src ───┘└─────┘ └──┘└─────┘└┘ ┴ └───
typ ───┘└─────┘ └──┘└─────┘└┘ ┴┴ └───
doc ───┘└─────┘ └──┘└─────┘└┘ ┴ └───
txt ───┘└─────┘ └──┘ └┘ ┴ └───
par ───┘└─────┘ └──┘ └┘ ┴ └───
pid ──────────┘ └──┘ └┘ ┴ └───
st ──────────────────────────────────
303 (zero_lt_iff_ne_zero.2 $ ennreal.inv_ne_zero.2 $ ennreal.nat_ne_top _),
id └─────────────────┘ └─────────────────┘ └────────────────┘
src ─────┘ └─────────────────┘└─┘ ┴└─────────────────┘└─┘ ┴└────────────────┘└─┘└─
typ ─────┘ └─────────────────┘└─┘ ┴└─────────────────┘└─┘ ┴└────────────────┘└─┘└─
doc ─────┘ └─┘ ┴ └─┘ ┴ └─┘└─
txt ─────┘ └─┘ ┴ └─┘ ┴ └─┘└─
par ─────┘ └─┘ ┴ └─┘ ┴ └─┘└─
pid ─────┘ └─┘ ┴ └─┘ ┴ └────
st ───────────────────────────────────────────────────────────────────────────┘└─
304 rcases h _ this with ⟨t, ht⟩,
id ┴ └──┘
src ───┘└─────┘ └─┘ └───────────┘└─
typ ───┘└─────┘┴└─┘└──┘└───────────┘└─
doc ───┘└─────┘ └─┘ └───────────┘└─
txt ───┘└─────┘ └─┘ └───────────┘└─
par ───┘└─────┘ └─┘ └───────────┘└─
pid ──────────┘ └─┘ └──────────────
st ───────────────────────────────┘└─
305 use [t],
id ┴
src ───┘└───┘ ┴└─
typ ───┘└───┘┴┴└─
doc ───┘└───┘ ┴└─
txt ───┘└───┘ ┴└─
par ───┘└───┘ ┴└─
pid ────────┘ └──
st ──────────┘└─
306 simpa [(>), infi_lt_iff, -add_comm] using ht },
id ┴ └─────────┘ └┘
src ───┘└─────┘┴└──┘└─────────┘└─────────────────┘ ┴┴
typ ───┘└─────┘┴└──┘└─────────┘└─────────────────┘└┘┴┴
doc ───┘└─────┘ └──┘ └─────────────────┘ ┴┴
txt ───┘└─────┘ └──┘ └─────────────────┘ ┴┴
par ───┘└─────┘ └──┘ └─────────────────┘ ┴┴
pid ──────────┘ └──┘ └─────────────────┘ └┘
st ────────────────────────────────────────────────┘└┘└
307 refine ⟨⋂n, t n, subset_Inter (λn, (ht n).1), is_measurable.Inter (λn, (ht n).2.1), _⟩,
id ┴ ┴ ┴ └──────────┘ └─────────────────┘ └┘
src └─────┘ ┴┴┴┴ ┴ └┘└──────────┘┴ └─┘ ┴ └────┘└─────────────────┘┴ └─┘ ┴ └────────┘
typ └─────┘ ┴┴┴┴┴┴ └┘└──────────┘┴ └─┘ ┴ └────┘└─────────────────┘┴ └─┘ └┘┴ └────────┘
doc └─────┘ ┴┴┴┴ ┴ └┘ ┴ └─┘ ┴ └────┘ ┴ └─┘ ┴ └────────┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └────┘ ┴ └─┘ ┴ └────────┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └────┘ ┴ └─┘ ┴ └────────┘
pid ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └────┘ ┴ └─┘ ┴ └────────┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
308 refine eq_of_le_of_forall_le_of_dense bot_le (assume r hr, _),
id └────────────────────────────┘ └────┘
src └─────┘└────────────────────────────┘┴└────┘┴ └───────┘
typ └─────┘└────────────────────────────┘┴└────┘┴ └───────┘
doc └─────┘ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └───────┘
st ──────────────────────────────────────────────────────────────┘└─
309 rcases ennreal.exists_inv_nat_lt (ne_of_gt hr) with ⟨n, hn⟩,
id └───────────────────────┘ └──────┘ └┘
src └─────┘└───────────────────────┘┴ └──────┘┴ └────────────┘
typ └─────┘└───────────────────────┘┴ └──────┘┴└┘└────────────┘
doc └─────┘ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └────────────┘
st ────────────────────────────────────────────────────────────┘└─
310 calc μ (⋂n, t n) ≤ μ (t n) : measure_mono (Inter_subset _ _)
id └──┘ ┴ ┴ ┴ └──────────┘ └──────────┘
src └──┘ └──────────┘ └──────────┘
typ └──┘ ┴ ┴ ┴ └──────────┘ └──────────┘
doc └──┘
st ───────────────────────────────────────────────────────────────
311 ... ≤ n⁻¹ : le_of_lt (ht n).2.2
id └┘ ┴ ┴ ┴
src ┴ ┴
typ └┘ ┴ ┴ ┴
st ────────────────────────────────────
312 ... ≤ r : le_of_lt hn
id ┴ └──────┘ └┘
src └──────┘
typ ┴ └──────┘ └┘
st ────────────────────────┘└
313 end
st ──┘
314
315 theorem measure_Union_le {β} [encodable β] (s : β → set α) : μ (⋃i, s i) ≤ (∑i, μ (s i)) :=
id └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc └───────┘ ┴ ┴ ┴ ┴
316 μ.to_outer_measure.Union _
id ┴└───────────────┘└────┘
src └───────────────┘└────┘
typ ┴└───────────────┘└────┘
317
318 lemma measure_Union_null {β} [encodable β] {s : β → set α} :
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
319 (∀ i, μ (s i) = 0) → μ (⋃i, s i) = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴
320 μ.to_outer_measure.Union_null
id ┴└───────────────┘└─────────┘
src └───────────────┘└─────────┘
typ ┴└───────────────┘└─────────┘
321
322 theorem measure_union_le (s₁ s₂ : set α) : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ :=
id └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
323 μ.to_outer_measure.union _ _
id ┴└───────────────┘└────┘
src └───────────────┘└────┘
typ ┴└───────────────┘└────┘
324
325 lemma measure_union_null {s₁ s₂ : set α} : μ s₁ = 0 → μ s₂ = 0 → μ (s₁ ∪ s₂) = 0 :=
id └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
326 μ.to_outer_measure.union_null
id ┴└───────────────┘└─────────┘
src └───────────────┘└─────────┘
typ ┴└───────────────┘└─────────┘
327
328 lemma measure_Union {β} [encodable β] {f : β → set α}
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
329 (hn : pairwise (disjoint on f)) (h : ∀i, is_measurable (f i)) :
id └──────┘ └──────┘ └┘ ┴ ┴ └───────────┘ ┴ ┴
src └──────┘ └──────┘ └┘ └───────────┘
typ └──────┘ └──────┘ └┘ ┴ ┴ └───────────┘ ┴ ┴
doc └──────┘ └──────┘ └───────────┘
330 μ (⋃i, f i) = (∑i, μ (f i)) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
331 by rw [measure_eq_measure' (is_measurable.Union h),
id └─────────────────┘ └─────────────────┘ ┴
src └──┘└─────────────────┘┴ └─────────────────┘┴ └──
typ └──┘└─────────────────┘┴ └─────────────────┘┴┴└──
doc └──┘ ┴ ┴ └──
txt └──┘ ┴ ┴ └──
par └──┘ ┴ ┴ └──
pid └┘ ┴ ┴ └──
st └──────────────────────────────────────────────┘└─
332 measure'_Union (λ s _, μ s) _ μ.m_Union hn h];
id └────────────┘ └───────┘ └┘ ┴
src ────┘└────────────┘┴ └────┘ ┴ └──┘└───────┘┴ ┴ ┴
typ ────┘└────────────┘┴ └────┘ ┴ └──┘└───────┘┴└┘┴┴┴
doc ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴
txt ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴
par ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴
pid ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴
st ────────────────────────────────────────────────┘┴└─
333 simp [measure_eq_measure', h]
id └─────────────────┘ ┴
src └────┘└─────────────────┘└┘ └─
typ └────┘└─────────────────┘└┘┴└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ─────────────────────────────────
334
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
335 lemma measure_union (hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
id └──────┘ └┘ └┘ └───────────┘ └┘ └───────────┘ └┘
src └──────┘ └───────────┘ └───────────┘
typ └──────┘ └┘ └┘ └───────────┘ └┘ └───────────┘ └┘
doc └──────┘ └───────────┘ └───────────┘
336 μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
id ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
337 by rw [measure_eq_measure' (h₁.union h₂),
id └─────────────────┘ └──────┘ └┘
src └──┘└─────────────────┘┴ └──────┘┴ └──
typ └──┘└─────────────────┘┴ └──────┘┴└┘└──
doc └──┘ ┴ ┴ └──
txt └──┘ ┴ ┴ └──
par └──┘ ┴ ┴ └──
pid └┘ ┴ ┴ └──
st └────────────────────────────────────┘└─
338 measure'_union (λ s _, μ s) _ μ.m_Union hd h₁ h₂];
id └────────────┘ └───────┘ └┘ └┘ └┘
src ────┘└────────────┘┴ └────┘ ┴ └──┘└───────┘┴ ┴ ┴ ┴
typ ────┘└────────────┘┴ └────┘ ┴ └──┘└───────┘┴└┘┴└┘┴└┘┴
doc ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴
txt ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴
par ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴
pid ────┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────┘┴└─
339 simp [measure_eq_measure', h₁, h₂]
id └─────────────────┘ └┘ └┘
src └────┘└─────────────────┘└┘ └┘ └─
typ └────┘└─────────────────┘└┘└┘└┘└┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ──────────────────────────────────────
340
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
341 lemma measure_bUnion {s : set β} {f : β → set α} (hs : countable s)
id └─┘ ┴ ┴ └─┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ └─┘ ┴ ┴ └─┘ ┴ └───────┘ ┴
doc └───────┘
342 (hd : pairwise_on s (disjoint on f)) (h : ∀b∈s, is_measurable (f b)) :
id └─────────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └─────────┘ └──────┘ └┘ ┴ └───────────┘
typ └─────────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────┘ └──────┘ └───────────┘
343 μ (⋃b∈s, f b) = ∑p:s, μ (f p.1) :=
id ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴
doc ┴ ┴ ┴ ┴
344 begin
st └─────
345 haveI := hs.to_encodable,
id └─────────────┘
src └───────┘└─────────────┘
typ └───────┘└─────────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ─────────────────────────┘└─
346 rw [← measure_Union, bUnion_eq_Union],
id └───────────┘ └─────────────┘
src └────┘└───────────┘└┘└─────────────┘┴
typ └────┘└───────────┘└┘└─────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ────────────────────┘└───────────────┘└──
347 { rintro ⟨i, hi⟩ ⟨j, hj⟩ ij x ⟨h₁, h₂⟩,
src └──────────────────────────────────┘
typ └──────────────────────────────────┘
doc └──────────────────────────────────┘
txt └──────────────────────────────────┘
par └──────────────────────────────────┘
pid └────────────────────────────┘
st ───┘└──────────────────────────────────┘└─
348 exact hd i hi j hj (mt subtype.eq' ij:_) ⟨h₁, h₂⟩ },
id └┘ ┴ └┘ ┴ └┘ └┘ └─────────┘ └┘ └┘ └┘
src └────┘ ┴ ┴ ┴ ┴ ┴ └┘┴└─────────┘┴ └──┘ └┘ └┘
typ └────┘└┘┴┴┴└┘┴┴┴└┘┴ └┘┴└─────────┘┴└┘└──┘ └┘└┘└┘└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ ┴┴
st ─────────────────────────────────────────────────────┘└┘└
349 { simpa }
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└─
350 end
st ──┘
351
352 lemma measure_sUnion {S : set (set α)} (hs : countable S)
id └─┘ └─┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ └─┘ └─┘ ┴ └───────┘ ┴
doc └───────┘
353 (hd : pairwise_on S disjoint) (h : ∀s∈S, is_measurable s) :
id └─────────┘ ┴ └──────┘ ┴ ┴ └───────────┘ ┴
src └─────────┘ └──────┘ └───────────┘
typ └─────────┘ ┴ └──────┘ ┴ ┴ └───────────┘ ┴
doc └─────────┘ └──────┘ └───────────┘
354 μ (⋃₀ S) = ∑s:S, μ s.1 :=
id ┴ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc ┴ ┴
355 by rw [sUnion_eq_bUnion, measure_bUnion hs hd h]
id └──────────────┘ └────────────┘ └┘ └┘ ┴
src └──┘└──────────────┘└┘└────────────┘┴ ┴ ┴ └─
typ └──┘└──────────────┘└┘└────────────┘┴└┘┴└┘┴┴└─
doc └──┘ └┘ ┴ ┴ ┴ └─
txt └──┘ └┘ ┴ ┴ ┴ └─
par └──┘ └┘ ┴ ┴ ┴ └─
pid └┘ └┘ ┴ ┴ ┴ ┴└
st └───────────────────┘└──────────────────────┘┴└
356
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
357 lemma measure_diff {s₁ s₂ : set α} (h : s₂ ⊆ s₁)
id └─┘ ┴ └┘ ┴ └┘
src └─┘ ┴
typ └─┘ ┴ └┘ ┴ └┘
358 (h₁ : is_measurable s₁) (h₂ : is_measurable s₂)
id └───────────┘ └┘ └───────────┘ └┘
src └───────────┘ └───────────┘
typ └───────────┘ └┘ └───────────┘ └┘
doc └───────────┘ └───────────┘
359 (h_fin : μ s₂ < ⊤) : μ (s₁ \ s₂) = μ s₁ - μ s₂ :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
360 begin
st └─────
361 refine (ennreal.add_sub_self' h_fin).symm.trans _,
id └───────────────────┘ └───┘
src └─────┘ └───────────────────┘┴ └────────────┘
typ └─────┘ └───────────────────┘┴└───┘└────────────┘
doc └─────┘ ┴ └────────────┘
txt └─────┘ ┴ └────────────┘
par └─────┘ ┴ └────────────┘
pid ┴ ┴ └────────────┘
st ──────────────────────────────────────────────────┘└─
362 rw [← measure_union disjoint_diff h₂ (h₁.diff h₂), union_diff_cancel h]
id └───────────┘ └───────────┘ └─────┘ └┘ └───────────────┘ ┴
src └────┘└───────────┘┴└───────────┘┴ ┴ └─────┘┴ └─┘└───────────────┘┴ └┘
typ └────┘└───────────┘┴└───────────┘┴ ┴ └─────┘┴└┘└─┘└───────────────┘┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
pid └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴┴
st ──────────────────────────────────────────────────┘└───────────────────┘┴┴
363 end
st └─┘
364
365 lemma measure_Union_eq_supr_nat {s : ℕ → set α} (h : ∀i, is_measurable (s i)) (hs : monotone s) :
id ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ ┴
src ┴ └─┘ └───────────┘ └──────┘
typ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └──────┘
366 μ (⋃i, s i) = (⨆i, μ (s i)) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
367 begin
st └─────
368 refine le_antisymm _ (supr_le $ λ i, measure_mono $ subset_Union _ _),
id └─────────┘ └─────┘ └──────────┘ └──────────┘
src └─────┘└─────────┘└─┘ └─────┘┴ ┴ └──┘└──────────┘┴ ┴└──────────┘└───┘
typ └─────┘└─────────┘└─┘ └─────┘┴ ┴ └──┘└──────────┘┴ ┴└──────────┘└───┘
doc └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └───┘
txt └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └───┘
par └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └───┘
pid ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ └───┘
st ──────────────────────────────────────────────────────────────────────┘└─
369 rw [← Union_disjointed,
id └──────────────┘
src └────┘└──────────────┘└─
typ └────┘└──────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid └──┘ └─
st ───────────────────────┘└─
370 measure_Union disjoint_disjointed (is_measurable.disjointed h),
id └───────────┘ └─────────────────┘ └──────────────────────┘ ┴
src ───┘└───────────┘┴└─────────────────┘┴ └──────────────────────┘┴ └──
typ ───┘└───────────┘┴└─────────────────┘┴ └──────────────────────┘┴┴└──
doc ───┘ ┴ ┴ ┴ └──
txt ───┘ ┴ ┴ ┴ └──
par ───┘ ┴ ┴ ┴ └──
pid ───┘ ┴ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────────┘└─
371 ennreal.tsum_eq_supr_nat],
id └──────────────────────┘
src ───┘└──────────────────────┘┴
typ ───┘└──────────────────────┘┴
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ───────────────────────────┘└──
372 refine supr_le (λ n, _),
id └─────┘
src └─────┘└─────┘┴ └────┘
typ └─────┘└─────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ────────────────────────┘└─
373 cases n, {apply zero_le _},
id ┴ └─────┘
src └────┘ └────┘└─────┘└┘
typ └────┘┴ └────┘└─────┘└┘
doc └────┘ └────┘ └┘
txt └────┘ └────┘ └┘
par └────┘ └────┘ └┘
pid ┴ ┴ └┘
st ────────┘└────────────────┘└┘└
374 suffices : sum (finset.range n.succ) (λ i, μ (disjointed s i)) = μ (s n),
id └─┘ └──────────┘ └────┘ └────────┘ ┴ ┴ ┴ ┴
src └─────────┘└─┘┴ └──────────┘┴└────┘└┘ └──┘ ┴ └────────┘┴ ┴ └─┘┴┴ ┴ ┴ ┴
typ └─────────┘└─┘┴ └──────────┘┴└────┘└┘ └──┘ ┴ └────────┘┴ ┴ └─┘┴┴┴┴ ┴┴┴┴
doc └─────────┘ ┴ └──────────┘┴ └┘ └──┘ ┴ └────────┘┴ ┴ └─┘ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
pid └───────┘└┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
375 { rw this, exact le_supr _ n },
id └──┘ └─────┘ ┴
src └─┘ └────┘└─────┘└─┘ ┴
typ └─┘└──┘ └────┘└─────┘└─┘┴┴
doc └─┘ └────┘ └─┘ ┴
txt └─┘ └────┘ └─┘ ┴
par └─┘ └────┘ └─┘ ┴
pid ┴ ┴ └─┘ ┴
st ───┘└─────┘└──────────────────┘└┘└
376 rw [← Union_disjointed_of_mono hs, measure_Union, tsum_eq_sum],
id └──────────────────────┘ └┘ └───────────┘ └─────────┘
src └────┘└──────────────────────┘┴ └┘└───────────┘└┘└─────────┘┴
typ └────┘└──────────────────────┘┴└┘└┘└───────────┘└┘└─────────┘┴
doc └────┘ ┴ └┘ └┘ ┴
txt └────┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ ┴
st ──────────────────────────────────┘└─────────────┘└───────────┘└──
377 { apply sum_congr rfl, intros i hi,
id └───────┘ └─┘
src └────┘└───────┘┴└─┘ └─────────┘
typ └────┘└───────┘┴└─┘ └─────────┘
doc └────┘ ┴ └─────────┘
txt └────┘ ┴ └─────────┘
par └────┘ ┴ └─────────┘
pid ┴ ┴ └───┘
st ───┘└─────────────────┘└───────────┘└─
378 simp [finset.mem_range.1 hi] },
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘ └┘
typ └────┘└──────────────┘└─┘└┘└┘
doc └────┘ └─┘ └┘
txt └────┘ └─┘ └┘
par └────┘ └─┘ └┘
pid ┴┴ └─┘ ┴┴
st ────────────────────────────────┘└┘└
379 { intros i hi, simp [mt finset.mem_range.2 hi] },
id └┘ └──────────────┘ └┘
src └─────────┘ └────┘└┘┴└──────────────┘└─┘ └┘
typ └─────────┘ └────┘└┘┴└──────────────┘└─┘└┘└┘
doc └─────────┘ └────┘ ┴ └─┘ └┘
txt └─────────┘ └────┘ ┴ └─┘ └┘
par └─────────┘ └────┘ ┴ └─┘ └┘
pid └───┘ ┴┴ ┴ └─┘ ┴┴
st ───┘└─────────┘└────────────────────────────────┘└┘└
380 { rintro i j ij x ⟨⟨_, ⟨_, rfl⟩, h₁⟩, ⟨_, ⟨_, rfl⟩, h₂⟩⟩,
src └────────────────────────────────────────────────────┘
typ └────────────────────────────────────────────────────┘
doc └────────────────────────────────────────────────────┘
txt └────────────────────────────────────────────────────┘
par └────────────────────────────────────────────────────┘
pid └──────────────────────────────────────────────┘
st ───┘└────────────────────────────────────────────────────┘└─
381 exact disjoint_disjointed i j ij ⟨h₁, h₂⟩ },
id └─────────────────┘ ┴ ┴ └┘ └┘ └┘
src └────┘└─────────────────┘┴ ┴ ┴ ┴ └┘ └┘
typ └────┘└─────────────────┘┴┴┴┴┴└┘┴ └┘└┘└┘└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴┴
st ─────────────────────────────────────────────┘└┘└
382 { intro i,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
383 by_cases h' : i < n.succ; simp [h', is_measurable.empty],
id ┴ ┴ └────┘ └┘ └─────────────────┘
src └───────┘ └─┘ ┴┴┴└────┘ └────┘ └┘└─────────────────┘┴
typ └───────┘ └─┘┴┴┴┴└────┘ └────┘└┘└┘└─────────────────┘┴
doc └───────┘ └─┘ ┴ ┴ └────┘ └┘ ┴
txt └───────┘ └─┘ ┴ ┴ └────┘ └┘ ┴
par └───────┘ └─┘ ┴ ┴ └────┘ └┘ ┴
pid ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴
st ───────────────────────────────────────────────────────────┘└─
384 apply is_measurable.disjointed h }
id └──────────────────────┘ ┴
src └────┘└──────────────────────┘┴ ┴
typ └────┘└──────────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────┘└─
385 end
st ──┘
386
387 lemma measure_Inter_eq_infi_nat {s : ℕ → set α}
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
388 (h : ∀i, is_measurable (s i)) (hs : ∀i j, i ≤ j → s j ⊆ s i)
id ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
389 (hfin : ∃i, μ (s i) < ⊤) :
id ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴ ┴
390 μ (⋂i, s i) = (⨅i, μ (s i)) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
391 begin
st └─────
392 rcases hfin with ⟨k, hk⟩,
id └──┘
src └─────┘ └───────────┘
typ └─────┘└──┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ─────────────────────────┘└─
393 rw [← ennreal.sub_sub_cancel (by exact hk) (infi_le _ k),
id └────────────────────┘ └┘ └─────┘ ┴
src └────┘└────────────────────┘┴ ┴└────┘ └┘ └─────┘└─┘ └──
typ └────┘└────────────────────┘┴ ┴└────┘└┘└┘ └─────┘└─┘┴└──
doc └────┘ ┴ ┴└────┘ └┘ └─┘ └──
txt └────┘ ┴ ┴└────┘ └┘ └─┘ └──
par └────┘ ┴ ┴└────┘ └┘ └─┘ └──
pid └──┘ ┴ └─────┘ └┘ └─┘ └──
st ─────────────────────────────────┘└───────┘└─────────────┘└─
394 ennreal.sub_infi,
id └──────────────┘
src ───┘└──────────────┘└─
typ ───┘└──────────────┘└─
doc ───┘ └─
txt ───┘ └─
par ───┘ └─
pid ───┘ └─
st ───────────────────┘└─
395 ← ennreal.sub_sub_cancel (by exact hk) (measure_mono (Inter_subset _ k)),
id └────────────────────┘ └┘ └──────────┘ └──────────┘ ┴
src ─────┘└────────────────────┘┴ ┴└────┘ └┘ └──────────┘┴ └──────────┘└─┘ └───
typ ─────┘└────────────────────┘┴ ┴└────┘└┘└┘ └──────────┘┴ └──────────┘└─┘┴└───
doc ─────┘ ┴ ┴└────┘ └┘ ┴ └─┘ └───
txt ─────┘ ┴ ┴└────┘ └┘ ┴ └─┘ └───
par ─────┘ ┴ ┴└────┘ └┘ ┴ └─┘ └───
pid ─────┘ ┴ └─────┘ └┘ ┴ └─┘ └───
st ───────────────────────────────┘└───────┘└─────────────────────────────────┘└─
396 ← measure_diff (Inter_subset _ k) (h k) (is_measurable.Inter h)
id └──────────┘ └─────────────────┘ ┴
src ─────┘└──────────┘┴ └─┘ └┘ ┴ └┘ └─────────────────┘┴ └─
typ ─────┘└──────────┘┴ └─┘ └┘ ┴ └┘ └─────────────────┘┴┴└─
doc ─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └─
txt ─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └─
par ─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └─
pid ─────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └─
st ────────────────────────────────────────────────────────────────────
397 (lt_of_le_of_lt (measure_mono (Inter_subset _ k)) hk),
id └────────────┘ └──────────┘ └──────────┘ ┴ └┘
src ─────┘ └────────────┘┴ └──────────┘┴ └──────────┘└─┘ └─┘ └──
typ ─────┘ └────────────┘┴ └──────────┘┴ └──────────┘└─┘┴└─┘└┘└──
doc ─────┘ ┴ ┴ └─┘ └─┘ └──
txt ─────┘ ┴ ┴ └─┘ └─┘ └──
par ─────┘ ┴ ┴ └─┘ └─┘ └──
pid ─────┘ ┴ ┴ └─┘ └─┘ └──
st ──────────────────────────────────────────────────────────┘└─
398 diff_Inter, measure_Union_eq_supr_nat],
id └────────┘ └───────────────────────┘
src ───┘└────────┘└┘└───────────────────────┘┴
typ ───┘└────────┘└┘└───────────────────────┘┴
doc ───┘ └┘ ┴
txt ───┘ └┘ ┴
par ───┘ └┘ ┴
pid ───┘ └┘ ┴
st ─────────────┘└─────────────────────────┘└──
399 { congr, funext i,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └┘
st ───┘└───┘└────────┘└─
400 cases le_total k i with ik ik,
id └──────┘ ┴ ┴
src └────┘└──────┘┴ ┴ └─────────┘
typ └────┘└──────┘┴┴┴┴└─────────┘
doc └────┘ ┴ ┴ └─────────┘
txt └────┘ ┴ ┴ └─────────┘
par └────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ────────────────────────────────┘└─
401 { exact measure_diff (hs _ _ ik) (h k) (h i)
id └──────────┘ ┴ ┴ ┴
src └────┘└──────────┘┴ └───┘ └┘ ┴ └┘ ┴ └─
typ └────┘└──────────┘┴ └───┘ └┘ ┴┴└┘ ┴┴┴└─
doc └────┘ ┴ └───┘ └┘ ┴ └┘ ┴ └─
txt └────┘ ┴ └───┘ └┘ ┴ └┘ ┴ └─
par └────┘ ┴ └───┘ └┘ ┴ └┘ ┴ └─
pid ┴ ┴ └───┘ └┘ ┴ └┘ ┴ └─
st ─────┘└──────────────────────────────────────────
402 (lt_of_le_of_lt (measure_mono (hs _ _ ik)) hk) },
id └────────────┘ └──────────┘ └┘ └┘ └┘
src ───────┘ └────────────┘┴ └──────────┘┴ └───┘ └─┘ └┘
typ ───────┘ └────────────┘┴ └──────────┘┴ └┘└───┘└┘└─┘└┘└┘
doc ───────┘ ┴ ┴ └───┘ └─┘ └┘
txt ───────┘ ┴ ┴ └───┘ └─┘ └┘
par ───────┘ ┴ ┴ └───┘ └─┘ └┘
pid ───────┘ ┴ ┴ └───┘ └─┘ ┴┴
st ──────────────────────────────────────────────────────┘└┘└
403 { rw [diff_eq_empty.2 (hs _ _ ik), measure_empty,
id └───────────┘ └┘ └┘ └───────────┘
src └──┘└───────────┘└─┘ └───┘ └─┘└───────────┘└─
typ └──┘└───────────┘└─┘ └┘└───┘└┘└─┘└───────────┘└─
doc └──┘ └─┘ └───┘ └─┘ └─
txt └──┘ └─┘ └───┘ └─┘ └─
par └──┘ └─┘ └───┘ └─┘ └─
pid └┘ └─┘ └───┘ └─┘ └─
st ────────────────────────────────────┘└─────────────┘└─
404 ennreal.sub_eq_zero_of_le (measure_mono (hs _ _ ik))] } },
id └───────────────────────┘ └──────────┘ └┘ └┘
src ─────┘└───────────────────────┘┴ └──────────┘┴ └───┘ └──┘
typ ─────┘└───────────────────────┘┴ └──────────┘┴ └┘└───┘└┘└──┘
doc ─────┘ ┴ ┴ └───┘ └──┘
txt ─────┘ ┴ ┴ └───┘ └──┘
par ─────┘ ┴ ┴ └───┘ └──┘
pid ─────┘ ┴ ┴ └───┘ └─┘┴
st ─────────────────────────────────────────────────────────┘┴┴└──┘└
405 { exact λ i, (h k).diff (h i) },
id ┴ ┴
src └────┘ └──┘ ┴ └─────┘ ┴ └┘
typ └────┘ └──┘ ┴┴└─────┘ ┴┴ └┘
doc └────┘ └──┘ ┴ └─────┘ ┴ └┘
txt └────┘ └──┘ ┴ └─────┘ ┴ └┘
par └────┘ └──┘ ┴ └─────┘ ┴ └┘
pid ┴ └──┘ ┴ └─────┘ ┴ ┴┴
st ───┘└──────────────────────────┘└┘└
406 { exact λ i j ij, diff_subset_diff_right (hs _ _ ij) }
id └────────────────────┘ └┘
src └────┘ └───────┘└────────────────────┘┴ └───┘ └┘
typ └────┘ └───────┘└────────────────────┘┴ └┘└───┘ └┘
doc └────┘ └───────┘ ┴ └───┘ └┘
txt └────┘ └───────┘ ┴ └───┘ └┘
par └────┘ └───────┘ ┴ └───┘ └┘
pid ┴ └───────┘ ┴ └───┘ ┴┴
st ──────────────────────────────────────────────────────┘└─
407 end
st ──┘
408
409 lemma measure_eq_inter_diff {μ : measure α} {s t : set α}
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
410 (hs : is_measurable s) (ht : is_measurable t) :
id └───────────┘ ┴ └───────────┘ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
411 μ s = μ (s ∩ t) + μ (s \ t) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
412 have hd : disjoint (s ∩ t) (s \ t) := assume a ⟨⟨_, hs⟩, _, hns⟩, hns hs ,
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
doc └──────┘
413 by rw [← measure_union hd (hs.inter ht) (hs.diff ht), inter_union_diff s t]
id └───────────┘ └┘ └──────┘ └─────┘ └┘ └──────────────┘ ┴ ┴
src └────┘└───────────┘┴ ┴ └──────┘┴ └┘ └─────┘┴ └─┘└──────────────┘┴ ┴ └─
typ └────┘└───────────┘┴└┘┴ └──────┘┴ └┘ └─────┘┴└┘└─┘└──────────────┘┴┴┴┴└─
doc └────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └─
txt └────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └─
par └────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └─
pid └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴└
st └────────────────────────────────────────────────┘└────────────────────┘┴└
414
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
415 lemma tendsto_measure_Union {μ : measure α} {s : ℕ → set α}
id └─────┘ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ └─────┘ ┴ ┴ └─┘ ┴
416 (hs : ∀n, is_measurable (s n)) (hm : monotone s) :
id ┴ └───────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └──────┘
typ ┴ └───────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └──────┘
417 tendsto (μ ∘ s) at_top (𝓝 (μ (⋃n, s n))) :=
id └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴┴ ┴ ┴
src └─────┘ ┴ └────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴┴ ┴ ┴
doc └─────┘ └────┘ ┴ ┴ ┴
418 begin
st └─────
419 rw measure_Union_eq_supr_nat hs hm,
id └───────────────────────┘ └┘ └┘
src └─┘└───────────────────────┘┴ ┴
typ └─┘└───────────────────────┘┴└┘┴└┘
doc └─┘ ┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────────────────┘└─
420 exact tendsto_at_top_supr_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm $ hnm)
id └─────────────────────┘ ┴ ┴ ┴ └──────────┘ └┘
src └────┘└─────────────────────┘┴ ┴┴┴ └┘ └────────┘└──────────┘┴ ┴ ┴ ┴ └┘
typ └────┘└─────────────────────┘┴ ┴┴┴┴┴└┘ └────────┘└──────────┘┴ ┴└┘┴ ┴ └┘
doc └────┘ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ ┴ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────┘
421 end
st └─┘
422
423 lemma tendsto_measure_Inter {μ : measure α} {s : ℕ → set α}
id └─────┘ ┴ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ └─────┘ ┴ ┴ └─┘ ┴
424 (hs : ∀n, is_measurable (s n)) (hm : ∀n m, n ≤ m → s m ⊆ s n) (hf : ∃i, μ (s i) < ⊤) :
id ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
425 tendsto (μ ∘ s) at_top (𝓝 (μ (⋂n, s n))) :=
id └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴┴ ┴ ┴
src └─────┘ ┴ └────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴┴ ┴ ┴
doc └─────┘ └────┘ ┴ ┴ ┴
426 begin
st └─────
427 rw measure_Inter_eq_infi_nat hs hm hf,
id └───────────────────────┘ └┘ └┘ └┘
src └─┘└───────────────────────┘┴ ┴ ┴
typ └─┘└───────────────────────┘┴└┘┴└┘┴└┘
doc └─┘ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
428 exact tendsto_at_top_infi_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm _ _ $ hnm),
id └─────────────────────┘ ┴ ┴ ┴ └──────────┘ └┘
src └────┘└─────────────────────┘┴ ┴┴┴ └┘ └────────┘└──────────┘┴ ┴ └───┘ ┴ ┴
typ └────┘└─────────────────────┘┴ ┴┴┴┴┴└┘ └────────┘└──────────┘┴ ┴└┘└───┘ ┴ ┴
doc └────┘ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ └───┘ ┴ ┴
txt └────┘ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ └───┘ ┴ ┴
par └────┘ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ └───┘ ┴ ┴
pid ┴ ┴ ┴ ┴ └┘ └────────┘ ┴ ┴ └───┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
429 end
st ──┘
430
431 end
432
433 def outer_measure.to_measure {α} (m : outer_measure α)
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
434 [ms : measurable_space α] (h : ms ≤ m.caratheodory) :
id └──────────────┘ ┴ └┘ ┴ ┴└───────────┘
src └──────────────┘ ┴ └───────────┘
typ └──────────────┘ ┴ └┘ ┴ ┴└───────────┘
doc └───────────┘
435 measure α :=
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
436 measure.of_measurable (λ s _, m s) m.empty
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴└────┘
src └───────────────────┘ └────┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴└────┘
437 (λ f hf hd, m.Union_eq_of_caratheodory (λ i, h _ (hf i)) hd)
id ┴ └┘ └┘ ┴└───────────────────────┘ ┴ ┴ └┘ ┴ └┘
src └───────────────────────┘
typ ┴ └┘ └┘ ┴└───────────────────────┘ ┴ ┴ └┘ ┴ └┘
438
439 lemma le_to_outer_measure_caratheodory {α} [ms : measurable_space α]
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
440 (μ : measure α) : ms ≤ μ.to_outer_measure.caratheodory :=
id └─────┘ ┴ └┘ ┴ ┴└───────────────┘└───────────┘
src └─────┘ ┴ └───────────────┘└───────────┘
typ └─────┘ ┴ └┘ ┴ ┴└───────────────┘└───────────┘
doc └───────────┘
441 begin
st └─────
442 assume s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
443 rw to_outer_measure_eq_outer_measure',
id └────────────────────────────────┘
src └─┘└────────────────────────────────┘
typ └─┘└────────────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────────────────┘└─
444 refine outer_measure.caratheodory_is_measurable (λ t, le_infi $ λ ht, _),
id └──────────────────────────────────────┘ └─────┘
src └─────┘└──────────────────────────────────────┘┴ └──┘└─────┘┴ ┴ └─────┘
typ └─────┘└──────────────────────────────────────┘┴ └──┘└─────┘┴ ┴ └─────┘
doc └─────┘ ┴ └──┘ ┴ ┴ └─────┘
txt └─────┘ ┴ └──┘ ┴ ┴ └─────┘
par └─────┘ ┴ └──┘ ┴ ┴ └─────┘
pid ┴ ┴ └──┘ ┴ ┴ └─────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
445 rw [← measure_eq_measure' (ht.inter hs),
id └─────────────────┘ └──────┘ └┘
src └────┘└─────────────────┘┴ └──────┘┴ └──
typ └────┘└─────────────────┘┴ └──────┘┴└┘└──
doc └────┘ ┴ ┴ └──
txt └────┘ ┴ ┴ └──
par └────┘ ┴ ┴ └──
pid └──┘ ┴ ┴ └──
st ────────────────────────────────────────┘└─
446 ← measure_eq_measure' (ht.diff hs),
id └─────────────────┘ └─────┘ └┘
src ─────┘└─────────────────┘┴ └─────┘┴ └──
typ ─────┘└─────────────────┘┴ └─────┘┴└┘└──
doc ─────┘ ┴ ┴ └──
txt ─────┘ ┴ ┴ └──
par ─────┘ ┴ ┴ └──
pid ─────┘ ┴ ┴ └──
st ─────────────────────────────────────┘└─
447 ← measure_union _ (ht.inter hs) (ht.diff hs),
id └───────────┘ └──────┘ └─────┘ └┘
src ─────┘└───────────┘└─┘ └──────┘┴ └┘ └─────┘┴ └──
typ ─────┘└───────────┘└─┘ └──────┘┴ └┘ └─────┘┴└┘└──
doc ─────┘ └─┘ ┴ └┘ ┴ └──
txt ─────┘ └─┘ ┴ └┘ ┴ └──
par ─────┘ └─┘ ┴ └┘ ┴ └──
pid ─────┘ └─┘ ┴ └┘ ┴ └──
st ───────────────────────────────────────────────┘└─
448 inter_union_diff],
id └──────────────┘
src ───┘└──────────────┘┴
typ ───┘└──────────────┘┴
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ───────────────────┘└──
449 exact le_refl _,
id └─────┘
src └────┘└─────┘└┘
typ └────┘└─────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ────────────────┘└─
450 exact λ x ⟨⟨_, h₁⟩, _, h₂⟩, h₂ h₁
id └┘ └┘
src └────┘ └──┘ └─┘ └────┘ └─┘ ┴ ┴
typ └────┘ └──┘ └─┘└┘└────┘└┘└─┘ ┴ ┴
doc └────┘ └──┘ └─┘ └────┘ └─┘ ┴ ┴
txt └────┘ └──┘ └─┘ └────┘ └─┘ ┴ ┴
par └────┘ └──┘ └─┘ └────┘ └─┘ ┴ ┴
pid ┴ └──┘ └─┘ └────┘ └─┘ ┴ ┴
st ───────────────────────────────────┘
451 end
st └─┘
452
453 lemma to_measure_to_outer_measure {α} (m : outer_measure α)
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
454 [ms : measurable_space α] (h : ms ≤ m.caratheodory) :
id └──────────────┘ ┴ └┘ ┴ ┴└───────────┘
src └──────────────┘ ┴ └───────────┘
typ └──────────────┘ ┴ └┘ ┴ ┴└───────────┘
doc └───────────┘
455 (m.to_measure h).to_outer_measure = m.trim := rfl
id ┴└─────────┘ ┴ └──────────────┘ ┴ ┴└───┘ └─┘
src └─────────┘ └──────────────┘ ┴ └───┘ └─┘
typ ┴└─────────┘ ┴ └──────────────┘ ┴ ┴└───┘ └─┘
456
457 @[simp] lemma to_measure_apply {α} (m : outer_measure α)
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └──┘
458 [ms : measurable_space α] (h : ms ≤ m.caratheodory)
id └──────────────┘ ┴ └┘ ┴ ┴└───────────┘
src └──────────────┘ ┴ └───────────┘
typ └──────────────┘ ┴ └┘ ┴ ┴└───────────┘
doc └───────────┘
459 {s : set α} (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
460 m.to_measure h s = m s := m.trim_eq hs
id ┴└─────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ └┘
src └─────────┘ ┴ └──────┘
typ ┴└─────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ └┘
461
462 lemma to_outer_measure_to_measure {α : Type*} [ms : measurable_space α] {μ : measure α} :
id └──────────────┘ ┴ └─────┘ ┴
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ └─────┘ ┴
463 μ.to_outer_measure.to_measure (le_to_outer_measure_caratheodory _) = μ :=
id ┴└───────────────┘└─────────┘ └──────────────────────────────┘ ┴ ┴
src └───────────────┘└─────────┘ └──────────────────────────────┘ ┴
typ ┴└───────────────┘└─────────┘ └──────────────────────────────┘ ┴ ┴
464 measure.ext $ λ s, μ.to_outer_measure.trim_eq
id └─────────┘ ┴ ┴└───────────────┘└──────┘
src └─────────┘ └───────────────┘└──────┘
typ └─────────┘ ┴ ┴└───────────────┘└──────┘
465
466 namespace measure
467 variables {α : Type*} {β : Type*} {γ : Type*}
id ┴
typ ┴
468 [measurable_space α] [measurable_space β] [measurable_space γ]
id └──────────────┘ └──────────────┘ └──────────────┘
src └──────────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ └──────────────┘ └──────────────┘
469
470 instance : has_zero (measure α) :=
id └──────┘ └─────┘ ┴
src └──────┘ └─────┘
typ └──────┘ └─────┘ ┴
471 ⟨{ to_outer_measure := 0,
472 m_Union := λ f hf hd, tsum_zero.symm,
id ┴ └┘ └┘ └───────┘└───┘
src └───────┘└───┘
typ ┴ └┘ └┘ └───────┘└───┘
473 trimmed := outer_measure.trim_zero }⟩
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
474
475 @[simp] theorem zero_to_outer_measure :
doc └──┘
476 (0 : measure α).to_outer_measure = 0 := rfl
id └─────┘ ┴ └──────────────┘ ┴ └─┘
src └─────┘ └──────────────┘ ┴ └─┘
typ └─────┘ ┴ └──────────────┘ ┴ └─┘
477
478 @[simp] theorem zero_apply (s : set α) : (0 : measure α) s = 0 := rfl
id └─┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
src └─┘ └─────┘ ┴ └─┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
doc └──┘
479
480 instance : inhabited (measure α) := ⟨0⟩
id └───────┘ └─────┘ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴
481
482 instance : has_add (measure α) :=
id └─────┘ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴
483 ⟨λμ₁ μ₂, {
id └┘ └┘
typ └┘ └┘
484 to_outer_measure := μ₁.to_outer_measure + μ₂.to_outer_measure,
id └┘└───────────────┘ ┴ └┘└───────────────┘
src └───────────────┘ ┴ └───────────────┘
typ └┘└───────────────┘ ┴ └┘└───────────────┘
485 m_Union := λs hs hd,
id ┴ └┘ └┘
typ ┴ └┘ └┘
486 show μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑ i, μ₁ (s i) + μ₂ (s i),
id └┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
487 by rw [ennreal.tsum_add, measure_Union hd hs, measure_Union hd hs],
id └──────────────┘ └───────────┘ └┘ └┘ └───────────┘ └┘ └┘
src └──┘└──────────────┘└┘└───────────┘┴ ┴ └┘└───────────┘┴ ┴ ┴
typ └──┘└──────────────┘└┘└───────────┘┴└┘┴└┘└┘└───────────┘┴└┘┴└┘┴
doc └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴
par └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴
pid └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴
st └───────────────────┘└───────────────────┘└───────────────────┘┴
488 trimmed := by rw [outer_measure.trim_add, μ₁.trimmed, μ₂.trimmed] }⟩
id └────────────────────┘
src └──┘└────────────────────┘└┘ └┘ └┘
typ └──┘└────────────────────┘└┘└────────┘└┘└────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └─────────────────────────┘└──────────┘└──────────┘┴┴
489
490 @[simp] theorem add_to_outer_measure (μ₁ μ₂ : measure α) :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └──┘
491 (μ₁ + μ₂).to_outer_measure = μ₁.to_outer_measure + μ₂.to_outer_measure := rfl
id └┘ ┴ └┘ └──────────────┘ ┴ └┘└───────────────┘ ┴ └┘└───────────────┘ └─┘
src ┴ └──────────────┘ ┴ └───────────────┘ ┴ └───────────────┘ └─┘
typ └┘ ┴ └┘ └──────────────┘ ┴ └┘└───────────────┘ ┴ └┘└───────────────┘ └─┘
492
493 @[simp] theorem add_apply (μ₁ μ₂ : measure α) (s : set α) :
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
doc └──┘
494 (μ₁ + μ₂) s = μ₁ s + μ₂ s := rfl
id └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘
495
496 instance add_comm_monoid : add_comm_monoid (measure α) :=
id └─────────────┘ └─────┘ ┴
src └─────────────┘ └─────┘
typ └─────────────┘ └─────┘ ┴
497 { zero := 0,
498 add := (+),
id ┴
src ┴
typ ┴
499 add_assoc := assume a b c, ext $ assume s hs, add_assoc _ _ _,
id ┴ ┴ ┴ └─┘ ┴ └┘ └───────┘
src └─┘ └───────┘
typ ┴ ┴ ┴ └─┘ ┴ └┘ └───────┘
500 add_comm := assume a b, ext $ assume s hs, add_comm _ _,
id ┴ ┴ └─┘ ┴ └┘ └──────┘
src └─┘ └──────┘
typ ┴ ┴ └─┘ ┴ └┘ └──────┘
501 zero_add := assume a, ext $ assume s hs, zero_add _,
id ┴ └─┘ ┴ └┘ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └┘ └──────┘
502 add_zero := assume a, ext $ assume s hs, add_zero _ }
id ┴ └─┘ ┴ └┘ └──────┘
src └─┘ └──────┘
typ ┴ └─┘ ┴ └┘ └──────┘
503
504 instance : partial_order (measure α) :=
id └───────────┘ └─────┘ ┴
src └───────────┘ └─────┘
typ └───────────┘ └─────┘ ┴
505 { le := λm₁ m₂, ∀ s, is_measurable s → m₁ s ≤ m₂ s,
id ┴ └┘ └┘ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ └───────────┘ ┴
typ ┴ └┘ └┘ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴
doc └───────────┘
506 le_refl := assume m s hs, le_refl _,
id ┴ ┴ └┘ └─────┘
src └─────┘
typ ┴ ┴ └┘ └─────┘
507 le_trans := assume m₁ m₂ m₃ h₁ h₂ s hs, le_trans (h₁ s hs) (h₂ s hs),
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ └┘ ┴ └┘
src └──────┘
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └──────┘ └┘ ┴ └┘ └┘ ┴ └┘
508 le_antisymm := assume m₁ m₂ h₁ h₂, ext $
id └┘ └┘ └┘ └┘ └─┘
src └─┘
typ └┘ └┘ └┘ └┘ └─┘
509 assume s hs, le_antisymm (h₁ s hs) (h₂ s hs) }
id ┴ └┘ └─────────┘ └┘ ┴ └┘ └┘ ┴ └┘
src └─────────┘
typ ┴ └┘ └─────────┘ └┘ ┴ └┘ └┘ ┴ └┘
510
511 theorem le_iff {μ₁ μ₂ : measure α} :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
512 μ₁ ≤ μ₂ ↔ ∀ s, is_measurable s → μ₁ s ≤ μ₂ s := iff.rfl
id └┘ ┴ └┘ ┴ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴ └─────┘
src ┴ ┴ └───────────┘ ┴ └─────┘
typ └┘ ┴ └┘ ┴ ┴ └───────────┘ ┴ └┘ ┴ ┴ └┘ ┴ └─────┘
doc └───────────┘
513
514 theorem to_outer_measure_le {μ₁ μ₂ : measure α} :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
515 μ₁.to_outer_measure ≤ μ₂.to_outer_measure ↔ μ₁ ≤ μ₂ :=
id └┘└───────────────┘ ┴ └┘└───────────────┘ ┴ └┘ ┴ └┘
src └───────────────┘ ┴ └───────────────┘ ┴ ┴
typ └┘└───────────────┘ ┴ └┘└───────────────┘ ┴ └┘ ┴ └┘
516 by rw [← μ₂.trimmed, outer_measure.le_trim_iff]; refl
id └───────────────────────┘
src └────┘ └┘└───────────────────────┘┴ └────
typ └────┘└────────┘└┘└───────────────────────┘┴ └────
doc └────┘ └┘ ┴ └────
txt └────┘ └┘ ┴ └────
par └────┘ └┘ ┴ └────
pid └──┘ └┘ ┴ └
st └───────────────┘└─────────────────────────┘┴└──────
517
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
518 theorem le_iff' {μ₁ μ₂ : measure α} :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
519 μ₁ ≤ μ₂ ↔ ∀ s, μ₁ s ≤ μ₂ s :=
id └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
520 to_outer_measure_le.symm
id └─────────────────┘└───┘
src └─────────────────┘└───┘
typ └─────────────────┘└───┘
521
522 section
523 variables {m : set (measure α)} {μ : measure α}
id └─┘ └─────┘ └─────┘
src └─┘ └─────┘ └─────┘
typ └─┘ └─────┘ └─────┘
524
525 lemma Inf_caratheodory (s : set α) (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
526 (Inf (measure.to_outer_measure '' m)).caratheodory.is_measurable s :=
id └─┘ └──────────────────────┘ └┘ ┴ └──────────┘ └───────────┘ ┴
src └─┘ └──────────────────────┘ └┘ └──────────┘ └───────────┘
typ └─┘ └──────────────────────┘ └┘ ┴ └──────────┘ └───────────┘ ┴
doc └─┘ └──────────┘
527 begin
st └─────
528 rw [outer_measure.Inf_eq_of_function_Inf_gen],
id └──────────────────────────────────────┘
src └──┘└──────────────────────────────────────┘┴
typ └──┘└──────────────────────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────────────────────────────┘└──
529 refine outer_measure.caratheodory_is_measurable (assume t, _),
id └──────────────────────────────────────┘
src └─────┘└──────────────────────────────────────┘┴ └────┘
typ └─────┘└──────────────────────────────────────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ──────────────────────────────────────────────────────────────┘└─
530 cases t.eq_empty_or_nonempty with ht ht, by simp [ht],
id └────────────────────┘ └┘
src └────┘└────────────────────┘└─────────┘ └────┘ ┴
typ └────┘└────────────────────┘└─────────┘ └────┘└┘┴
doc └────┘ └─────────┘ └────┘ ┴
txt └────┘ └─────────┘ └────┘ ┴
par └────┘ └─────────┘ └────┘ ┴
pid ┴ └─────────┘ ┴┴ ┴
st ────────────────────────────────────────┘ └─
531 simp only [outer_measure.Inf_gen_nonempty1 _ _ ht, le_infi_iff, ball_image_iff,
id └─────────────────────────────┘ └┘ └─────────┘ └────────────┘
src └─────────┘└─────────────────────────────┘└───┘ └┘└─────────┘└┘└────────────┘└─
typ └─────────┘└─────────────────────────────┘└───┘└┘└┘└─────────┘└┘└────────────┘└─
doc └─────────┘ └───┘ └┘ └┘ └─
txt └─────────┘ └───┘ └┘ └┘ └─
par └─────────┘ └───┘ └┘ └┘ └─
pid ┴└──┘└┘ └───┘ └┘ └┘ └─
st ──────────────────────────────────────────────────────────────────────────────────
532 to_outer_measure_apply, measure_eq_infi t],
id └────────────────────┘ └─────────────┘ ┴
src ───┘└────────────────────┘└┘└─────────────┘┴ ┴
typ ───┘└────────────────────┘└┘└─────────────┘┴┴┴
doc ───┘ └┘ ┴ ┴
txt ───┘ └┘ ┴ ┴
par ───┘ └┘ ┴ ┴
pid ───┘ └┘ ┴ ┴
st ─────────────────────────────────────────────┘└─
533 assume μ hμ u htu hu,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──────────────────┘
st ─────────────────────┘└─
534 have hm : ∀{s t}, s ⊆ t → outer_measure.Inf_gen (to_outer_measure '' m) s ≤ μ t,
id ┴ └───────────────────┘ └──────────────┘ └┘ ┴ ┴ ┴
src └────────┘ └───┘ ┴ ┴┴┴ ┴ ┴└───────────────────┘┴ └──────────────┘┴└┘┴ └┘ ┴┴┴ ┴
typ └────────┘ └───┘ ┴ ┴┴┴ ┴ ┴└───────────────────┘┴ └──────────────┘┴└┘┴┴└┘ ┴┴┴┴┴
doc └────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └─────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
535 { assume s t hst,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───┘└────────────┘└─
536 rw [outer_measure.Inf_gen_nonempty2 _ _ (mem_image_of_mem _ hμ)],
id └─────────────────────────────┘ └──────────────┘ └┘
src └──┘└─────────────────────────────┘└───┘ └──────────────┘└─┘ └┘
typ └──┘└─────────────────────────────┘└───┘ └──────────────┘└─┘└┘└┘
doc └──┘ └───┘ └─┘ └┘
txt └──┘ └───┘ └─┘ └┘
par └──┘ └───┘ └─┘ └┘
pid └┘ └───┘ └─┘ └┘
st ──────────────────────────────────────────────────────────────────┘└──
537 refine infi_le_of_le (μ.to_outer_measure) (infi_le_of_le (mem_image_of_mem _ hμ) _),
id └────────────────┘ └───────────┘ └──────────────┘ └┘
src └─────┘ ┴ └────────────────┘└┘ └───────────┘┴ └──────────────┘└─┘ └──┘
typ └─────┘ ┴ └────────────────┘└┘ └───────────┘┴ └──────────────┘└─┘└┘└──┘
doc └─────┘ ┴ └┘ ┴ └─┘ └──┘
txt └─────┘ ┴ └┘ ┴ └─┘ └──┘
par └─────┘ ┴ └┘ ┴ └─┘ └──┘
pid ┴ ┴ └┘ ┴ └─┘ └──┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
538 rw [to_outer_measure_apply],
id └────────────────────┘
src └──┘└────────────────────┘┴
typ └──┘└────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ─────────────────────────────┘└──
539 refine measure_mono hst },
id └──────────┘ └─┘
src └─────┘└──────────┘┴ ┴
typ └─────┘└──────────┘┴└─┘┴
doc └─────┘ ┴ ┴
txt └─────┘ ┴ ┴
par └─────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────────┘└┘└
540 rw [measure_eq_inter_diff hu hs],
id └───────────────────┘ └┘ └┘
src └──┘└───────────────────┘┴ ┴ ┴
typ └──┘└───────────────────┘┴└┘┴└┘┴
doc └──┘ ┴ ┴ ┴
txt └──┘ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴
st ────────────────────────────────┘└──
541 refine add_le_add' (hm $ inter_subset_inter_left _ htu) (hm $ diff_subset_diff_left htu)
id └─────────┘ └─────────────────────┘ └┘ └───────────────────┘ └─┘
src └─────┘└─────────┘┴ ┴ ┴└─────────────────────┘└─┘ └┘ ┴ ┴└───────────────────┘┴ └┘
typ └─────┘└─────────┘┴ ┴ ┴└─────────────────────┘└─┘ └┘ └┘┴ ┴└───────────────────┘┴└─┘└┘
doc └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘
542 end
st └─┘
543
544 instance : has_Inf (measure α) :=
id └─────┘ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴
doc └─────┘
545 ⟨λm, (Inf (to_outer_measure '' m)).to_measure $ Inf_caratheodory⟩
id ┴ └─┘ └──────────────┘ └┘ ┴ └────────┘ └──────────────┘
src └─┘ └──────────────┘ └┘ └────────┘ └──────────────┘
typ ┴ └─┘ └──────────────┘ └┘ ┴ └────────┘ └──────────────┘
doc └─┘
546
547 lemma Inf_apply {m : set (measure α)} {s : set α} (hs : is_measurable s) :
id └─┘ └─────┘ ┴ └─┘ ┴ └───────────┘ ┴
src └─┘ └─────┘ └─┘ └───────────┘
typ └─┘ └─────┘ ┴ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
548 Inf m s = Inf (to_outer_measure '' m) s :=
id └─┘ ┴ ┴ ┴ └─┘ └──────────────┘ └┘ ┴ ┴
src └─┘ ┴ └─┘ └──────────────┘ └┘
typ └─┘ ┴ ┴ ┴ └─┘ └──────────────┘ └┘ ┴ ┴
doc └─┘ └─┘
549 to_measure_apply _ _ hs
id └──────────────┘ └┘
src └──────────────┘
typ └──────────────┘ └┘
550
551 private lemma Inf_le (h : μ ∈ m) : Inf m ≤ μ :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
552 have Inf (to_outer_measure '' m) ≤ μ.to_outer_measure := Inf_le (mem_image_of_mem _ h),
id └─┘ └──────────────┘ └┘ ┴ ┴ ┴└───────────────┘ └────┘ └──────────────┘ ┴
src └─┘ └──────────────┘ └┘ ┴ └───────────────┘ └────┘ └──────────────┘
typ └─┘ └──────────────┘ └┘ ┴ ┴ ┴└───────────────┘ └────┘ └──────────────┘ ┴
doc └─┘
553 assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
id ┴ └┘ └───────┘ └┘ └────────────────────┘ └──┘ ┴
src └──┘└───────┘┴ └──┘└────────────────────┘┴ └────┘ ┴ └
typ ┴ └┘ └──┘└───────┘┴└┘└──┘└────────────────────┘┴ └────┘└──┘┴┴└
doc └──┘ ┴ └──┘ ┴ └────┘ ┴ └
txt └──┘ ┴ └──┘ ┴ └────┘ ┴ └
par └──┘ ┴ └──┘ ┴ └────┘ ┴ └
pid └┘ ┴ └──┘ ┴ ┴ ┴ └
st └───────────────┘└────────────────────────┘┴└──────────────
554
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
555 private lemma le_Inf (h : ∀μ' ∈ m, μ ≤ μ') : μ ≤ Inf m :=
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴
src ┴ ┴ └─┘
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴
doc └─┘
556 have μ.to_outer_measure ≤ Inf (to_outer_measure '' m) :=
id ┴└───────────────┘ ┴ └─┘ └──────────────┘ └┘ ┴
src └───────────────┘ ┴ └─┘ └──────────────┘ └┘
typ ┴└───────────────┘ ┴ └─┘ └──────────────┘ └┘ ┴
doc └─┘
557 le_Inf $ ball_image_of_ball $ assume μ hμ, to_outer_measure_le.2 $ h _ hμ,
id └────┘ └────────────────┘ ┴ └┘ └─────────────────┘┴ ┴ └┘
src └────┘ └────────────────┘ └─────────────────┘┴
typ └────┘ └────────────────┘ ┴ └┘ └─────────────────┘┴ ┴ └┘
558 assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
id ┴ └┘ └───────┘ └┘ └────────────────────┘ └──┘ ┴
src └──┘└───────┘┴ └──┘└────────────────────┘┴ └────┘ ┴ └
typ ┴ └┘ └──┘└───────┘┴└┘└──┘└────────────────────┘┴ └────┘└──┘┴┴└
doc └──┘ ┴ └──┘ ┴ └────┘ ┴ └
txt └──┘ ┴ └──┘ ┴ └────┘ ┴ └
par └──┘ ┴ └──┘ ┴ └────┘ ┴ └
pid └┘ ┴ └──┘ ┴ ┴ ┴ └
st └───────────────┘└────────────────────────┘┴└──────────────
559
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
560 instance : has_Sup (measure α) := ⟨λs, Inf {μ' | ∀μ∈s, μ ≤ μ' }⟩
id └─────┘ └─────┘ ┴ ┴ └─┘ ┴└┘ ┴ ┴ ┴ ┴ └┘
src └─────┘ └─────┘ └─┘ ┴ ┴
typ └─────┘ └─────┘ ┴ ┴ └─┘ ┴└┘ ┴ ┴ ┴ ┴ └┘
doc └─────┘ └─┘
561 private lemma le_Sup (h : μ ∈ m) : μ ≤ Sup m := le_Inf $ assume μ' h', h' _ h
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └────┘ └┘ └┘ └┘ ┴
src ┴ ┴ └─┘ └────┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └────┘ └┘ └┘ └┘ ┴
doc └─┘
562 private lemma Sup_le (h : ∀μ' ∈ m, μ' ≤ μ) : Sup m ≤ μ := Inf_le h
id └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────┘ ┴
src ┴ └─┘ ┴ └────┘
typ └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────┘ ┴
doc └─┘
563
564 instance : order_bot (measure α) :=
id └───────┘ └─────┘ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴
doc └───────┘
565 { bot := 0, bot_le := assume a s hs, bot_le, .. measure.partial_order }
id ┴ ┴ └┘ └────┘ └───────────────────┘
src └────┘ └───────────────────┘
typ ┴ ┴ └┘ └────┘ └───────────────────┘
566
567 instance : order_top (measure α) :=
id └───────┘ └─────┘ ┴
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴
doc └───────┘
568 { top := (⊤ : outer_measure α).to_measure (by rw [outer_measure.top_caratheodory]; exact le_top),
id ┴ └───────────┘ ┴ └────────┘ └────────────────────────────┘ └────┘
src ┴ └───────────┘ └────────┘ └──┘└────────────────────────────┘┴ └────┘└────┘
typ ┴ └───────────┘ ┴ └────────┘ └──┘└────────────────────────────┘┴ └────┘└────┘
doc └──┘ ┴ └────┘
txt └──┘ ┴ └────┘
par └──┘ ┴ └────┘
pid └┘ ┴ ┴
st └─────────────────────────────────┘┴└────────────┘
569 le_top := assume a s hs,
id ┴ ┴ └┘
typ ┴ ┴ └┘
570 by cases s.eq_empty_or_nonempty with h h;
id └────────────────────┘
src └────┘└────────────────────┘└────────┘
typ └────┘└────────────────────┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st └────────────────────────────────────────
571 simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply],
id ┴ └──────────────┘ ┴ └┘ └─────────────────────┘
src └────┘ └┘└──────────────┘┴┴└─┘ └┘└─────────────────────┘┴
typ └────┘┴└┘└──────────────┘┴┴└─┘└┘└┘└─────────────────────┘┴
doc └────┘ └┘ ┴ └─┘ └┘ ┴
txt └────┘ └┘ ┴ └─┘ └┘ ┴
par └────┘ └┘ ┴ └─┘ └┘ ┴
pid ┴┴ └┘ ┴ └─┘ └┘ ┴
st ───────────────────────────────────────────────────────────────┘
572 .. measure.partial_order }
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
573
574 instance : complete_lattice (measure α) :=
id └──────────────┘ └─────┘ ┴
src └──────────────┘ └─────┘
typ └──────────────┘ └─────┘ ┴
doc └──────────────┘
575 { Inf := Inf,
id └─┘
src └─┘
typ └─┘
doc └─┘
576 Sup := Sup,
id └─┘
src └─┘
typ └─┘
doc └─┘
577 inf := λa b, Inf {a, b},
id ┴ ┴ └─┘ ┴┴┴ ┴
src └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴┴┴ ┴
doc └─┘
578 sup := λa b, Sup {a, b},
id ┴ ┴ └─┘ ┴┴┴ ┴
src └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴┴┴ ┴
doc └─┘
579 le_Sup := assume s μ h, le_Sup h,
id ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └────┘ ┴
580 Sup_le := assume s μ h, Sup_le h,
id ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └────┘ ┴
581 Inf_le := assume s μ h, Inf_le h,
id ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └────┘ ┴
582 le_Inf := assume s μ h, le_Inf h,
id ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └────┘ ┴
583 le_sup_left := assume a b, le_Sup $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
584 le_sup_right := assume a b, le_Sup $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
585 sup_le := assume a b c hac hbc, Sup_le $ by simp [*, or_imp_distrib] {contextual := tt},
id ┴ ┴ ┴ └─┘ └─┘ └────┘ └────────────┘ └┘
src └────┘ └───────┘└────────────┘└┘ └────────────┘└┘┴
typ ┴ ┴ ┴ └─┘ └─┘ └────┘ └───────┘└────────────┘└┘ └────────────┘└┘┴
doc └───────┘ └┘ └────────────┘ ┴
txt └───────┘ └┘ └────────────┘ ┴
par └───────┘ └┘ └────────────┘ ┴
pid ┴└──┘ ┴┴ └────────────┘ ┴
st └──────────────────────────────────────────┘
586 inf_le_left := assume a b, Inf_le $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
587 inf_le_right := assume a b, Inf_le $ by simp,
id ┴ ┴ └────┘
src └────┘ └──┘
typ ┴ ┴ └────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
588 le_inf := assume a b c hac hbc, le_Inf $ by simp [*, or_imp_distrib] {contextual := tt},
id ┴ ┴ ┴ └─┘ └─┘ └────┘ └────────────┘ └┘
src └────┘ └───────┘└────────────┘└┘ └────────────┘└┘┴
typ ┴ ┴ ┴ └─┘ └─┘ └────┘ └───────┘└────────────┘└┘ └────────────┘└┘┴
doc └───────┘ └┘ └────────────┘ ┴
txt └───────┘ └┘ └────────────┘ ┴
par └───────┘ └┘ └────────────┘ ┴
pid ┴└──┘ ┴┴ └────────────┘ ┴
st └──────────────────────────────────────────┘
589 .. measure.partial_order, .. measure.lattice.order_top, .. measure.lattice.order_bot }
id └───────────────────┘ └───────────────────────┘ └───────────────────────┘
src └───────────────────┘ └───────────────────────┘ └───────────────────────┘
typ └───────────────────┘ └───────────────────────┘ └───────────────────────┘
590
591 end
592
593 def map (f : α → β) (μ : measure α) : measure β :=
id ┴ ┴ └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ ┴ ┴ └─────┘ ┴ └─────┘ ┴
594 if hf : measurable f then
id └┘ └────────┘ ┴
src └┘ └────────┘
typ └┘ └────────┘ ┴
doc └────────┘
595 (μ.to_outer_measure.map f).to_measure $ λ s hs t,
id ┴└───────────────┘└──┘ ┴ └────────┘ ┴ └┘ ┴
src └───────────────┘└──┘ └────────┘
typ ┴└───────────────┘└──┘ ┴ └────────┘ ┴ └┘ ┴
596 le_to_outer_measure_caratheodory μ _ (hf _ hs) (f ⁻¹' t)
id └──────────────────────────────┘ ┴ └┘ └┘ ┴ └─┘ ┴
src └──────────────────────────────┘ └─┘
typ └──────────────────────────────┘ ┴ └┘ └┘ ┴ └─┘ ┴
doc └─┘
597 else 0
id ┴
src ┴
typ ┴
598
599 variables {μ ν : measure α}
id └─────┘
src └─────┘
typ └─────┘
600
601 @[simp] theorem map_apply {f : α → β} (hf : measurable f)
id ┴ ┴ └────────┘ ┴
src └────────┘
typ ┴ ┴ └────────┘ ┴
doc └──┘ └────────┘
602 {s : set β} (hs : is_measurable s) :
id └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ └─┘ ┴ └───────────┘ ┴
doc └───────────┘
603 (map f μ : measure β) s = μ (f ⁻¹' s) :=
id └─┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ └─────┘ ┴ └─┘
typ └─┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─┘
604 by rw [map, dif_pos hf, to_measure_apply _ _ hs]; refl
id └─┘ └─────┘ └┘ └──────────────┘ └┘
src └──┘└─┘└┘└─────┘┴ └┘└──────────────┘└───┘ ┴ └────
typ └──┘└─┘└┘└─────┘┴└┘└┘└──────────────┘└───┘└┘┴ └────
doc └──┘ └┘ ┴ └┘ └───┘ ┴ └────
txt └──┘ └┘ ┴ └┘ └───┘ ┴ └────
par └──┘ └┘ ┴ └┘ └───┘ ┴ └────
pid └┘ └┘ ┴ └┘ └───┘ ┴ └
st └──────┘└──────────┘└───────────────────────┘┴└──────
605
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
606 @[simp] lemma map_id : map id μ = μ :=
id └─┘ └┘ ┴ ┴ ┴
src └─┘ └┘ ┴
typ └─┘ └┘ ┴ ┴ ┴
doc └──┘
607 ext $ λ s, map_apply measurable_id
id └─┘ ┴ └───────┘ └───────────┘
src └─┘ └───────┘ └───────────┘
typ └─┘ ┴ └───────┘ └───────────┘
608
609 lemma map_map {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
610 map g (map f μ) = map (g ∘ f) μ :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
611 ext $ λ s hs,
id └─┘ ┴ └┘
src └─┘
typ └─┘ ┴ └┘
612 by simp [hf, hg, hs, hg.preimage hs, hg.comp hf];
id └┘ └┘ └┘ └─────────┘ └┘ └─────┘ └┘
src └────┘ └┘ └┘ └┘└─────────┘┴ └┘└─────┘┴ ┴
typ └────┘└┘└┘└┘└┘└┘└┘└─────────┘┴└┘└┘└─────┘┴└┘┴
doc └────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴
txt └────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴
par └────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴
pid ┴┴ └┘ └┘ └┘ ┴ └┘ ┴ ┴
st └───────────────────────────────────────────────
613 rw ← preimage_comp
id └───────────┘
src └───┘└───────────┘└
typ └───┘└───────────┘└
doc └───┘ └
txt └───┘ └
par └───┘ └
pid └─┘ └
st ──────────────────────
614
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
615 /-- The dirac measure. -/
616 def dirac (a : α) : measure α :=
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
617 (outer_measure.dirac a).to_measure (by simp)
id └─────────────────┘ ┴ └────────┘
src └─────────────────┘ └────────┘ └──┘
typ └─────────────────┘ ┴ └────────┘ └──┘
doc └─────────────────┘ └──┘
txt └──┘
par └──┘
st └───┘
618
619 @[simp] lemma dirac_apply (a : α) {s : set α} (hs : is_measurable s) :
id ┴ └─┘ ┴ └───────────┘ ┴
src └─┘ └───────────┘
typ ┴ └─┘ ┴ └───────────┘ ┴
doc └──┘ └───────────┘
620 (dirac a : measure α) s = ⨆ h : a ∈ s, 1 :=
id └───┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └───┘ └─────┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └───┘ ┴ ┴
621 to_measure_apply _ _ hs
id └──────────────┘ └┘
src └──────────────┘
typ └──────────────┘ └┘
622
623 /-- Sum of an indexed family of measures. -/
624 def sum {ι : Type*} (f : ι → measure α) : measure α :=
id ┴ └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ ┴ └─────┘ ┴ └─────┘ ┴
625 (outer_measure.sum (λ i, (f i).to_outer_measure)).to_measure $
id └───────────────┘ ┴ ┴ ┴ └──────────────┘ └────────┘
src └───────────────┘ └──────────────┘ └────────┘
typ └───────────────┘ ┴ ┴ ┴ └──────────────┘ └────────┘
626 le_trans
id └──────┘
src └──────┘
typ └──────┘
627 (by exact le_infi (λ i, le_to_outer_measure_caratheodory _))
id └─────┘ └──────────────────────────────┘
src └────┘└─────┘┴ └──┘└──────────────────────────────┘└─┘
typ └────┘└─────┘┴ └──┘└──────────────────────────────┘└─┘
doc └────┘ ┴ └──┘ └─┘
txt └────┘ ┴ └──┘ └─┘
par └────┘ ┴ └──┘ └─┘
pid ┴ ┴ └──┘ └─┘
st └──────────────────────────────────────────────────────┘
628 (outer_measure.le_sum_caratheodory _)
id └───────────────────────────────┘
src └───────────────────────────────┘
typ └───────────────────────────────┘
629
630 /-- Counting measure on any measurable space. -/
631 def count : measure α := sum dirac
id └─────┘ ┴ └─┘ └───┘
src └─────┘ └─┘ └───┘
typ └─────┘ ┴ └─┘ └───┘
doc └─┘ └───┘
632
633 @[class] def is_complete {α} {_:measurable_space α} (μ : measure α) : Prop :=
id └──────────────┘ ┴ └─────┘ ┴
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ └─────┘ ┴
634 ∀ s, μ s = 0 → is_measurable s
id ┴ ┴ ┴ ┴ └───────────┘ ┴
src ┴ └───────────┘
typ ┴ ┴ ┴ ┴ └───────────┘ ┴
doc └───────────┘
635
636 /-- The "almost everywhere" filter of co-null sets. -/
637 def a_e (μ : measure α) : filter α :=
id └─────┘ ┴ └────┘ ┴
src └─────┘ └────┘
typ └─────┘ ┴ └────┘ ┴
638 { sets := {s | μ (-s) = 0},
id ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴
639 univ_sets := by simp [measure_empty],
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────┘
640 inter_sets := λ s t hs ht, by simp [compl_inter]; exact measure_union_null hs ht,
id ┴ ┴ └┘ └┘ └─────────┘ └────────────────┘ └┘ └┘
src └────┘└─────────┘┴ └────┘└────────────────┘┴ ┴
typ ┴ ┴ └┘ └┘ └────┘└─────────┘┴ └────┘└────────────────┘┴└┘┴└┘
doc └────┘ ┴ └────┘ ┴ ┴
txt └────┘ ┴ └────┘ ┴ ┴
par └────┘ ┴ └────┘ ┴ ┴
pid ┴┴ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────────┘
641 sets_of_superset := λ s t hs hst, measure_mono_null (set.compl_subset_compl.2 hst) hs }
id ┴ ┴ └┘ └─┘ └───────────────┘ └────────────────────┘┴ └─┘ └┘
src └───────────────┘ └────────────────────┘┴
typ ┴ ┴ └┘ └─┘ └───────────────┘ └────────────────────┘┴ └─┘ └┘
642
643 lemma mem_a_e_iff (s : set α) : s ∈ μ.a_e.sets ↔ μ (- s) = 0 := iff.rfl
id └─┘ ┴ ┴ ┴ ┴└──┘└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─┘ ┴ └──┘└───┘ ┴ ┴ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴└──┘└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘
644
645 end measure
646
647 end measure_theory
648
649 section is_complete
650 open measure_theory
651
652 variables {α : Type*} [measurable_space α] (μ : measure α)
id ┴ └──────────────┘ └─────┘
src └──────────────┘ └─────┘
typ ┴ └──────────────┘ └─────┘
653
654 def is_null_measurable (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
655 ∃ t z, s = t ∪ z ∧ is_measurable t ∧ μ z = 0
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
656
657 theorem is_null_measurable_iff {μ : measure α} {s : set α} :
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
658 is_null_measurable μ s ↔
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴
659 ∃ t, t ⊆ s ∧ is_measurable t ∧ μ (s \ t) = 0 :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
660 begin
st └─────
661 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
662 { rintro ⟨t, z, rfl, ht, hz⟩,
src └────────────────────────┘
typ └────────────────────────┘
doc └────────────────────────┘
txt └────────────────────────┘
par └────────────────────────┘
pid └──────────────────┘
st ───┘└────────────────────────┘└─
663 refine ⟨t, set.subset_union_left _ _, ht, measure_mono_null _ hz⟩,
id ┴ └───────────────────┘ └┘ └───────────────┘ └┘
src └─────┘ └┘└───────────────────┘└────┘ └┘└───────────────┘└─┘ ┴
typ └─────┘ ┴└┘└───────────────────┘└────┘└┘└┘└───────────────┘└─┘└┘┴
doc └─────┘ └┘ └────┘ └┘ └─┘ ┴
txt └─────┘ └┘ └────┘ └┘ └─┘ ┴
par └─────┘ └┘ └────┘ └┘ └─┘ ┴
pid ┴ └┘ └────┘ └┘ └─┘ ┴
st ────────────────────────────────────────────────────────────────────┘└─
664 simp [union_diff_left, diff_subset] },
id └─────────────┘ └─────────┘
src └────┘└─────────────┘└┘└─────────┘└┘
typ └────┘└─────────────┘└┘└─────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────────────────────────────────────┘└┘└
665 { rintro ⟨t, st, ht, hz⟩,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └──────────────┘
st ─────────────────────────┘└─
666 exact ⟨t, _, (union_diff_cancel st).symm, ht, hz⟩ }
id ┴ └───────────────┘ └┘ └┘ └┘
src └────┘ └───┘ └───────────────┘┴ └──────┘ └┘ └┘
typ └────┘ ┴└───┘ └───────────────┘┴└┘└──────┘└┘└┘└┘└┘
doc └────┘ └───┘ ┴ └──────┘ └┘ └┘
txt └────┘ └───┘ ┴ └──────┘ └┘ └┘
par └────┘ └───┘ ┴ └──────┘ └┘ └┘
pid ┴ └───┘ ┴ └──────┘ └┘ ┴┴
st ─────────────────────────────────────────────────────┘└─
667 end
st ──┘
668
669 theorem is_null_measurable_measure_eq {μ : measure α} {s t : set α}
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
670 (st : t ⊆ s) (hz : μ (s \ t) = 0) : μ s = μ t :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
671 begin
st └─────
672 refine le_antisymm _ (measure_mono st),
id └─────────┘ └──────────┘ └┘
src └─────┘└─────────┘└─┘ └──────────┘┴ ┴
typ └─────┘└─────────┘└─┘ └──────────┘┴└┘┴
doc └─────┘ └─┘ ┴ ┴
txt └─────┘ └─┘ ┴ ┴
par └─────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────────────────────────┘└─
673 have := measure_union_le t (s \ t),
id └──────────────┘ ┴ ┴ ┴
src └──────┘└──────────────┘┴ ┴ ┴┴┴ ┴
typ └──────┘└──────────────┘┴ ┴ ┴┴┴┴┴┴
doc └──────┘ ┴ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────┘└─
674 rw [union_diff_cancel st, hz] at this, simpa
id └───────────────┘ └┘ └┘
src └──┘└───────────────┘┴ └┘ └───────┘ └────┘
typ └──┘└───────────────┘┴└┘└┘└┘└───────┘ └────┘
doc └──┘ ┴ └┘ └───────┘ └────┘
txt └──┘ ┴ └┘ └───────┘ └────┘
par └──┘ ┴ └┘ └───────┘ └────┘
pid └┘ ┴ └┘ ┴└──────┘ ┴
st ─────────────────────────┘└──┘┴└──────┘└──────┘
675 end
st └─┘
676
677 theorem is_measurable.is_null_measurable
678 {s : set α} (hs : is_measurable s) : is_null_measurable μ s :=
id └─┘ ┴ └───────────┘ ┴ └────────────────┘ ┴ ┴
src └─┘ └───────────┘ └────────────────┘
typ └─┘ ┴ └───────────┘ ┴ └────────────────┘ ┴ ┴
doc └───────────┘
679 ⟨s, ∅, by simp, hs, μ.empty⟩
id ┴ ┴ └┘ ┴└────┘
src ┴ └──┘ └────┘
typ ┴ ┴ └──┘ └┘ ┴└────┘
doc └──┘
txt └──┘
par └──┘
st └───┘
680
681 theorem is_null_measurable_of_complete [c : μ.is_complete]
id ┴└──────────┘
src └──────────┘
typ ┴└──────────┘
682 {s : set α} : is_null_measurable μ s ↔ is_measurable s :=
id └─┘ ┴ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴
src └─┘ └────────────────┘ ┴ └───────────┘
typ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴
doc └───────────┘
683 ⟨by rintro ⟨t, z, rfl, ht, hz⟩; exact
src └────────────────────────┘ └─────
typ └────────────────────────┘ └─────
doc └────────────────────────┘ └─────
txt └────────────────────────┘ └─────
par └────────────────────────┘ └─────
pid └──────────────────┘ └
st └──────────────────────────────────
684 is_measurable.union ht (c _ hz),
id └─────────────────┘ └┘ ┴ └┘
src ─┘└─────────────────┘┴ ┴ └─┘ ┴
typ ─┘└─────────────────┘┴└┘┴ ┴└─┘└┘┴
doc ─┘ ┴ ┴ └─┘ ┴
txt ─┘ ┴ ┴ └─┘ ┴
par ─┘ ┴ ┴ └─┘ ┴
pid ─┘ ┴ ┴ └─┘ ┴
st ────────────────────────────────┘
685 λ h, h.is_null_measurable _⟩
id ┴ ┴└─────────────────┘
src └─────────────────┘
typ ┴ ┴└─────────────────┘
686
687 variables {μ}
688 theorem is_null_measurable.union_null {s z : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
689 (hs : is_null_measurable μ s) (hz : μ z = 0) :
id └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴
690 is_null_measurable μ (s ∪ z) :=
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴
691 begin
st └─────
692 rcases hs with ⟨t, z', rfl, ht, hz'⟩,
id └┘
src └─────┘ └─────────────────────────┘
typ └─────┘└┘└─────────────────────────┘
doc └─────┘ └─────────────────────────┘
txt └─────┘ └─────────────────────────┘
par └─────┘ └─────────────────────────┘
pid ┴ └─────────────────────────┘
st ─────────────────────────────────────┘└─
693 exact ⟨t, z' ∪ z, set.union_assoc _ _ _, ht, le_zero_iff_eq.1
id ┴ └┘ ┴ ┴ └─────────────┘ └┘ └────────────┘
src └────┘ └┘ ┴┴┴ └┘└─────────────┘└──────┘ └┘└────────────┘└──
typ └────┘ ┴└┘└┘┴┴┴┴└┘└─────────────┘└──────┘└┘└┘└────────────┘└──
doc └────┘ └┘ ┴ ┴ └┘ └──────┘ └┘ └──
txt └────┘ └┘ ┴ ┴ └┘ └──────┘ └┘ └──
par └────┘ └┘ ┴ ┴ └┘ └──────┘ └┘ └──
pid ┴ └┘ ┴ ┴ └┘ └──────┘ └┘ └──
st ────────────────────────────────────────────────────────────────
694 (le_trans (measure_union_le _ _) $ by simp [hz, hz'])⟩
id └──────┘ └──────────────┘ └┘ └─┘
src ───┘ └──────┘┴ └──────────────┘└────┘ ┴ ┴└────┘ └┘ ┴└─┘
typ ───┘ └──────┘┴ └──────────────┘└────┘ ┴ ┴└────┘└┘└┘└─┘┴└─┘
doc ───┘ ┴ └────┘ ┴ ┴└────┘ └┘ ┴└─┘
txt ───┘ ┴ └────┘ ┴ ┴└────┘ └┘ ┴└─┘
par ───┘ ┴ └────┘ ┴ ┴└────┘ └┘ ┴└─┘
pid ───┘ ┴ └────┘ ┴ └─────┘ └┘ └─┘┴
st ────────────────────────────────────────┘└─────────────┘└─┘
695 end
st └─┘
696
697 theorem null_is_null_measurable {z : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
698 (hz : μ z = 0) : is_null_measurable μ z :=
id ┴ ┴ ┴ └────────────────┘ ┴ ┴
src ┴ └────────────────┘
typ ┴ ┴ ┴ └────────────────┘ ┴ ┴
699 by simpa using (is_measurable.empty.is_null_measurable _).union_null hz
id └────────────────────────────────────┘ └┘
src └──────────┘ └────────────────────────────────────┘└─────────────┘ └
typ └──────────┘ └────────────────────────────────────┘└─────────────┘└┘└
doc └──────────┘ └─────────────┘ └
txt └──────────┘ └─────────────┘ └
par └──────────┘ └─────────────┘ └
pid ┴└────┘ └─────────────┘ └
st └─────────────────────────────────────────────────────────────────────
700
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
701 theorem is_null_measurable.Union_nat {s : ℕ → set α}
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
702 (hs : ∀ i, is_null_measurable μ (s i)) :
id ┴ └────────────────┘ ┴ ┴ ┴
src └────────────────┘
typ ┴ └────────────────┘ ┴ ┴ ┴
703 is_null_measurable μ (Union s) :=
id └────────────────┘ ┴ └───┘ ┴
src └────────────────┘ └───┘
typ └────────────────┘ ┴ └───┘ ┴
doc └───┘
704 begin
st └─────
705 choose t ht using assume i, is_null_measurable_iff.1 (hs i),
id └────────────────────┘ └┘
src └────────────────┘ └──┘└────────────────────┘└─┘ ┴ ┴
typ └────────────────┘ └──┘└────────────────────┘└─┘ └┘┴ ┴
doc └────────────────┘ └──┘ └─┘ ┴ ┴
txt └────────────────┘ └──┘ └─┘ ┴ ┴
par └────────────────┘ └──┘ └─┘ ┴ ┴
pid └┘└─┘└─────┘ └──┘ └─┘ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
706 simp [forall_and_distrib] at ht,
id └────────────────┘
src └────┘└────────────────┘└─────┘
typ └────┘└────────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ────────────────────────────────┘└─
707 rcases ht with ⟨st, ht, hz⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ────────────────────────────┘└─
708 refine is_null_measurable_iff.2
id └────────────────────┘
src └─────┘└────────────────────┘└──
typ └─────┘└────────────────────┘└──
doc └─────┘ └──
txt └─────┘ └──
par └─────┘ └──
pid ┴ └──
st ──────────────────────────────────
709 ⟨Union t, Union_subset_Union st, is_measurable.Union ht,
id └───┘ ┴ └────────────────┘ └┘ └─────────────────┘ └┘
src ───┘ └───┘┴ └┘└────────────────┘┴ └┘└─────────────────┘┴ └─
typ ───┘ └───┘┴┴└┘└────────────────┘┴└┘└┘└─────────────────┘┴└┘└─
doc ───┘ └───┘┴ └┘ ┴ └┘ ┴ └─
txt ───┘ ┴ └┘ ┴ └┘ ┴ └─
par ───┘ ┴ └┘ ┴ └┘ ┴ └─
pid ───┘ ┴ └┘ ┴ └┘ ┴ └─
st ─────────────────────────────────────────────────────────────
710 measure_mono_null _ (measure_Union_null hz)⟩,
id └───────────────┘ └────────────────┘ └┘
src ─────┘└───────────────┘└─┘ └────────────────┘┴ └┘
typ ─────┘└───────────────┘└─┘ └────────────────┘┴└┘└┘
doc ─────┘ └─┘ ┴ └┘
txt ─────┘ └─┘ ┴ └┘
par ─────┘ └─┘ ┴ └┘
pid ─────┘ └─┘ ┴ └┘
st ─────────────────────────────────────────────────┘└─
711 rw [diff_subset_iff, ← Union_union_distrib],
id └─────────────┘ └─────────────────┘
src └──┘└─────────────┘└──┘└─────────────────┘┴
typ └──┘└─────────────┘└──┘└─────────────────┘┴
doc └──┘ └──┘ ┴
txt └──┘ └──┘ ┴
par └──┘ └──┘ ┴
pid └┘ └──┘ ┴
st ────────────────────┘└─────────────────────┘└──
712 exact Union_subset_Union (λ i, by rw ← diff_subset_iff)
id └────────────────┘ └─────────────┘
src └────┘└────────────────┘┴ └──┘ ┴└───┘└─────────────┘└┘
typ └────┘└────────────────┘┴ └──┘ ┴└───┘└─────────────┘└┘
doc └────┘ ┴ └──┘ ┴└───┘ └┘
txt └────┘ ┴ └──┘ ┴└───┘ └┘
par └────┘ ┴ └──┘ ┴└───┘ └┘
pid ┴ ┴ └──┘ └────┘ ┴┴
st ──────────────────────────────────┘└───────────────────┘└┘
713 end
st └─┘
714
715 theorem is_measurable.diff_null {s z : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
716 (hs : is_measurable s) (hz : μ z = 0) :
id └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘
717 is_null_measurable μ (s \ z) :=
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴
718 begin
st └─────
719 rw measure_eq_infi at hz,
id └─────────────┘
src └─┘└─────────────┘└────┘
typ └─┘└─────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ─────────────────────────┘└─
720 choose f hf using show ∀ q : {q:ℚ//q>0}, ∃ t:set α,
id ┴ ┴ ┴ ┴ └─┘ ┴┴
src └────────────────┘ ┴ └───┘┴└┘┴└┘ ┴└┘ ┴┴└─┘└─┘┴ ┴└
typ └────────────────┘ ┴ └───┘┴└┘┴└┘ ┴└┘ ┴┴└─┘└─┘┴┴┴└
doc └────────────────┘ ┴ └───┘ └┘┴└┘ └┘ ┴ └─┘ ┴ └
txt └────────────────┘ ┴ └───┘ └┘ └┘ └┘ ┴ └─┘ ┴ └
par └────────────────┘ ┴ └───┘ └┘ └┘ └┘ ┴ └─┘ ┴ └
pid └┘└─┘└─────┘ ┴ └───┘ └┘ └┘ └┘ ┴ └─┘ ┴ └
st ──────────────────────────────────────────────────────
721 z ⊆ t ∧ is_measurable t ∧ μ t < (nnreal.of_real q.1 : ennreal),
id ┴ ┴ ┴ └───────────┘ ┴ ┴ └────────────┘ └─────┘
src ───┘ ┴┴┴ ┴┴┴└───────────┘┴ ┴ ┴ ┴ ┴┴┴ └────────────┘┴ └───┘└─────┘└──
typ ───┘┴┴┴┴ ┴┴┴└───────────┘┴ ┴ ┴┴┴ ┴┴┴ └────────────┘┴ └───┘└─────┘└──
doc ───┘ ┴ ┴ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└─────┘└──
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──
st ────────────────────────────────────────────────────────────────────
722 { rintro ⟨ε, ε0⟩,
src ───┘└────────────┘└─
typ ───┘└────────────┘└─
doc ───┘└────────────┘└─
txt ───┘└────────────┘└─
par ───┘└────────────┘└─
pid ────────────────────
st ──┘└─────────────┘└─
723 have : 0 < (nnreal.of_real ε : ennreal), { simpa using ε0 },
id └────────────┘ ┴ └─────┘ └┘
src ───┘└───────┘ ┴ └────────────┘┴ └─┘└─────┘┴└──┘└──────────┘ ┴└──
typ ───┘└───────┘ ┴ └────────────┘┴┴└─┘└─────┘┴└──┘└──────────┘└┘┴└──
doc ───┘└───────┘ ┴ ┴ └─┘└─────┘┴└──┘└──────────┘ ┴└──
txt ───┘└───────┘ ┴ ┴ └─┘ ┴└──┘└──────────┘ ┴└──
par ───┘└───────┘ ┴ ┴ └─┘ ┴└──┘└──────────┘ ┴└──
pid ────────────┘ ┴ ┴ └─┘ └───────────────┘ └───
st ──────────────────────────────────────────┘└─┘└──────────────┘┴└─
724 rw ← hz at this, simpa [infi_lt_iff] },
id └┘ └─────────┘
src ───┘└───┘ └──────┘└┘└─────┘└─────────┘└┘┴
typ ───┘└───┘└┘└──────┘└┘└─────┘└─────────┘└┘┴
doc ───┘└───┘ └──────┘└┘└─────┘ └┘┴
txt ───┘└───┘ └──────┘└┘└─────┘ └┘┴
par ───┘└───┘ └──────┘└┘└─────┘ └┘┴
pid ────────┘ └───────────────┘ └─┘
st ──────────────────┘└────────────────────┘└┘└
725 refine is_null_measurable_iff.2 ⟨s \ Inter f,
id └────────────────────┘ ┴ ┴ └───┘ ┴
src └─────┘└────────────────────┘└─┘ ┴┴┴└───┘┴ └─
typ └─────┘└────────────────────┘└─┘ ┴┴┴┴└───┘┴┴└─
doc └─────┘ └─┘ ┴ ┴└───┘┴ └─
txt └─────┘ └─┘ ┴ ┴ ┴ └─
par └─────┘ └─┘ ┴ ┴ ┴ └─
pid ┴ └─┘ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────
726 diff_subset_diff_right (subset_Inter (λ i, (hf i).1)),
id └────────────────────┘ └──────────┘
src ───┘└────────────────────┘┴ └──────────┘┴ └──┘ ┴ └──────
typ ───┘└────────────────────┘┴ └──────────┘┴ └──┘ ┴ └──────
doc ───┘ ┴ ┴ └──┘ ┴ └──────
txt ───┘ ┴ ┴ └──┘ ┴ └──────
par ───┘ ┴ ┴ └──┘ ┴ └──────
pid ───┘ ┴ ┴ └──┘ ┴ └──────
st ───────────────────────────────────────────────────────────
727 hs.diff (is_measurable.Inter (λ i, (hf i).2.1)),
id └─────┘ └─────────────────┘ └┘
src ───┘└─────┘┴ └─────────────────┘┴ └──┘ ┴ └────────
typ ───┘└─────┘┴ └─────────────────┘┴ └──┘ └┘┴ └────────
doc ───┘ ┴ ┴ └──┘ ┴ └────────
txt ───┘ ┴ ┴ └──┘ ┴ └────────
par ───┘ ┴ ┴ └──┘ ┴ └────────
pid ───┘ ┴ ┴ └──┘ ┴ └────────
st ─────────────────────────────────────────────────────
728 measure_mono_null _ (le_zero_iff_eq.1 $ le_of_not_lt $ λ h, _)⟩,
id └───────────────┘ └────────────┘ └──────────┘
src ───┘└───────────────┘└─┘ └────────────┘└─┘ ┴└──────────┘┴ ┴ └─────┘
typ ───┘└───────────────┘└─┘ └────────────┘└─┘ ┴└──────────┘┴ ┴ └─────┘
doc ───┘ └─┘ └─┘ ┴ ┴ ┴ └─────┘
txt ───┘ └─┘ └─┘ ┴ ┴ ┴ └─────┘
par ───┘ └─┘ └─┘ ┴ ┴ ┴ └─────┘
pid ───┘ └─┘ └─┘ ┴ ┴ ┴ └─────┘
st ──────────────────────────────────────────────────────────────────┘└─
729 { exact Inter f },
id └───┘ ┴
src └────┘└───┘┴ ┴
typ └────┘└───┘┴┴┴
doc └────┘└───┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───┘└────────────┘└┘└
730 { rw [diff_subset_iff, diff_union_self],
id └─────────────┘ └─────────────┘
src └──┘└─────────────┘└┘└─────────────┘┴
typ └──┘└─────────────┘└┘└─────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───┘└─────────────────┘└───────────────┘└──
731 exact subset.trans (diff_subset _ _) (subset_union_left _ _) },
id └──────────┘ └─────────┘ └───────────────┘
src └────┘└──────────┘┴ └─────────┘└────┘ └───────────────┘└────┘
typ └────┘└──────────┘┴ └─────────┘└────┘ └───────────────┘└────┘
doc └────┘ ┴ └────┘ └────┘
txt └────┘ ┴ └────┘ └────┘
par └────┘ ┴ └────┘ └────┘
pid ┴ ┴ └────┘ └───┘┴
st ────────────────────────────────────────────────────────────────┘└┘└
732 rcases ennreal.lt_iff_exists_rat_btwn.1 h with ⟨ε, ε0', ε0, h⟩,
id └────────────────────────────┘ ┴
src └─────┘└────────────────────────────┘└─┘ └───────────────────┘
typ └─────┘└────────────────────────────┘└─┘┴└───────────────────┘
doc └─────┘ └─┘ └───────────────────┘
txt └─────┘ └─┘ └───────────────────┘
par └─────┘ └─┘ └───────────────────┘
pid ┴ └─┘ └───────────────────┘
st ───────────────────────────────────────────────────────────────┘└─
733 simp at ε0,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ───────────┘└─
734 apply not_le_of_lt (lt_trans (hf ⟨ε, ε0⟩).2.2 h),
id └──────────┘ └──────┘ └┘ ┴ └┘ ┴
src └────┘└──────────┘┴ └──────┘┴ ┴ └┘ └─────┘ ┴
typ └────┘└──────────┘┴ └──────┘┴ └┘┴ ┴└┘└┘└─────┘┴┴
doc └────┘ ┴ ┴ ┴ └┘ └─────┘ ┴
txt └────┘ ┴ ┴ ┴ └┘ └─────┘ ┴
par └────┘ ┴ ┴ ┴ └┘ └─────┘ ┴
pid ┴ ┴ ┴ ┴ └┘ └─────┘ ┴
st ─────────────────────────────────────────────────┘└─
735 exact measure_mono (Inter_subset _ _)
id └──────────┘ └──────────┘
src └────┘└──────────┘┴ └──────────┘└────┘
typ └────┘└──────────┘┴ └──────────┘└────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴ ┴ └───┘┴
st ───────────────────────────────────────┘
736 end
st └─┘
737
738 theorem is_null_measurable.diff_null {s z : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
739 (hs : is_null_measurable μ s) (hz : μ z = 0) :
id └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴
740 is_null_measurable μ (s \ z) :=
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴
741 begin
st └─────
742 rcases hs with ⟨t, z', rfl, ht, hz'⟩,
id └┘
src └─────┘ └─────────────────────────┘
typ └─────┘└┘└─────────────────────────┘
doc └─────┘ └─────────────────────────┘
txt └─────┘ └─────────────────────────┘
par └─────┘ └─────────────────────────┘
pid ┴ └─────────────────────────┘
st ─────────────────────────────────────┘└─
743 rw [set.union_diff_distrib],
id └────────────────────┘
src └──┘└────────────────────┘┴
typ └──┘└────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────────────────┘└──
744 exact (ht.diff_null hz).union_null (measure_mono_null (diff_subset _ _) hz')
id └──────────┘ └┘ └───────────────┘ └─────────┘ └─┘
src └────┘ └──────────┘┴ └───────────┘ └───────────────┘┴ └─────────┘└────┘ └┘
typ └────┘ └──────────┘┴└┘└───────────┘ └───────────────┘┴ └─────────┘└────┘└─┘└┘
doc └────┘ ┴ └───────────┘ ┴ └────┘ └┘
txt └────┘ ┴ └───────────┘ ┴ └────┘ └┘
par └────┘ ┴ └───────────┘ ┴ └────┘ └┘
pid ┴ ┴ └───────────┘ ┴ └────┘ ┴┴
st ──────────────────────────────────────────────────────────────────────────────┘
745 end
st └─┘
746
747 theorem is_null_measurable.compl {s : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
748 (hs : is_null_measurable μ s) :
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
749 is_null_measurable μ (-s) :=
id └────────────────┘ ┴ ┴┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴┴
750 begin
st └─────
751 rcases hs with ⟨t, z, rfl, ht, hz⟩,
id └┘
src └─────┘ └───────────────────────┘
typ └─────┘└┘└───────────────────────┘
doc └─────┘ └───────────────────────┘
txt └─────┘ └───────────────────────┘
par └─────┘ └───────────────────────┘
pid ┴ └───────────────────────┘
st ───────────────────────────────────┘└─
752 rw compl_union,
id └─────────┘
src └─┘└─────────┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
753 exact ht.compl.diff_null hz
id └────────────────┘ └┘
src └────┘└────────────────┘┴ ┴
typ └────┘└────────────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────┘
754 end
st └─┘
755
756 def null_measurable {α : Type u} [measurable_space α]
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
757 (μ : measure α) : measurable_space α :=
id └─────┘ ┴ └──────────────┘ ┴
src └─────┘ └──────────────┘
typ └─────┘ ┴ └──────────────┘ ┴
758 { is_measurable := is_null_measurable μ,
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
759 is_measurable_empty := is_measurable.empty.is_null_measurable _,
id └─────────────────┘└─────────────────┘
src └─────────────────┘└─────────────────┘
typ └─────────────────┘└─────────────────┘
760 is_measurable_compl := λ s hs, hs.compl,
id ┴ └┘ └┘└────┘
src └────┘
typ ┴ └┘ └┘└────┘
761 is_measurable_Union := λ f, is_null_measurable.Union_nat }
id ┴ └──────────────────────────┘
src └──────────────────────────┘
typ ┴ └──────────────────────────┘
762
763 def completion {α : Type u} [measurable_space α] (μ : measure α) :
id └──────────────┘ ┴ └─────┘ ┴
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ └─────┘ ┴
764 @measure_theory.measure α (null_measurable μ) :=
id └────────────────────┘ ┴ └─────────────┘ ┴
src └────────────────────┘ └─────────────┘
typ └────────────────────┘ ┴ └─────────────┘ ┴
765 { to_outer_measure := μ.to_outer_measure,
id ┴└───────────────┘
src └───────────────┘
typ ┴└───────────────┘
766 m_Union := λ s hs hd, show μ (Union s) = ∑ i, μ (s i), begin
id ┴ └┘ └┘ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ └┘ └┘ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └───┘ ┴ ┴
st └─────
767 choose t ht using assume i, is_null_measurable_iff.1 (hs i),
id └────────────────────┘ └┘
src └────────────────┘ └──┘└────────────────────┘└─┘ ┴ ┴
typ └────────────────┘ └──┘└────────────────────┘└─┘ └┘┴ ┴
doc └────────────────┘ └──┘ └─┘ ┴ ┴
txt └────────────────┘ └──┘ └─┘ ┴ ┴
par └────────────────┘ └──┘ └─┘ ┴ ┴
pid └┘└─┘└─────┘ └──┘ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
768 simp [forall_and_distrib] at ht, rcases ht with ⟨st, ht, hz⟩,
id └────────────────┘ └┘
src └────┘└────────────────┘└─────┘ └─────┘ └────────────────┘
typ └────┘└────────────────┘└─────┘ └─────┘└┘└────────────────┘
doc └────┘ └─────┘ └─────┘ └────────────────┘
txt └────┘ └─────┘ └─────┘ └────────────────┘
par └────┘ └─────┘ └─────┘ └────────────────┘
pid ┴┴ ┴┴└───┘ ┴ └────────────────┘
st ──────────────────────────────────┘└───────────────────────────┘└─
769 rw is_null_measurable_measure_eq (Union_subset_Union st),
id └───────────────────────────┘ └────────────────┘ └┘
src └─┘└───────────────────────────┘┴ └────────────────┘┴ ┴
typ └─┘└───────────────────────────┘┴ └────────────────┘┴└┘┴
doc └─┘ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────┘└─
770 { rw measure_Union _ ht,
id └───────────┘ └┘
src └─┘└───────────┘└─┘
typ └─┘└───────────┘└─┘└┘
doc └─┘ └─┘
txt └─┘ └─┘
par └─┘ └─┘
pid ┴ └─┘
st ─────┘└───────────────────┘└─
771 { congr, funext i,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └┘
st ───────┘└───┘└────────┘└─
772 exact (is_null_measurable_measure_eq (st i) (hz i)).symm },
id └───────────────────────────┘ └┘ └┘ ┴
src └────┘ └───────────────────────────┘┴ ┴ └┘ ┴ └──────┘
typ └────┘ └───────────────────────────┘┴ └┘┴ └┘ └┘┴┴└──────┘
doc └────┘ ┴ ┴ └┘ ┴ └──────┘
txt └────┘ ┴ ┴ └┘ ┴ └──────┘
par └────┘ ┴ ┴ └┘ ┴ └──────┘
pid ┴ ┴ ┴ └┘ ┴ └────┘└┘
st ────────────────────────────────────────────────────────────────┘└┘└
773 { rintro i j ij x ⟨h₁, h₂⟩,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └────────────────┘
st ───────────────────────────────┘└─
774 exact hd i j ij ⟨st i h₁, st j h₂⟩ } },
id └┘ └┘ ┴ └┘ └┘ ┴ └┘
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
typ └────┘└┘┴ ┴ ┴└┘┴ ┴┴┴└┘└┘└┘┴┴┴└┘└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────┘└──┘└
775 { refine measure_mono_null _ (measure_Union_null hz),
id └───────────────┘ └────────────────┘ └┘
src └─────┘└───────────────┘└─┘ └────────────────┘┴ ┴
typ └─────┘└───────────────┘└─┘ └────────────────┘┴└┘┴
doc └─────┘ └─┘ ┴ ┴
txt └─────┘ └─┘ ┴ ┴
par └─────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
776 rw [diff_subset_iff, ← Union_union_distrib],
id └─────────────┘ └─────────────────┘
src └──┘└─────────────┘└──┘└─────────────────┘┴
typ └──┘└─────────────┘└──┘└─────────────────┘┴
doc └──┘ └──┘ ┴
txt └──┘ └──┘ ┴
par └──┘ └──┘ ┴
pid └┘ └──┘ ┴
st ────────────────────────┘└─────────────────────┘└──
777 exact Union_subset_Union (λ i, by rw ← diff_subset_iff) }
id └────────────────┘ └─────────────┘
src └────┘└────────────────┘┴ └──┘ ┴└───┘└─────────────┘└┘
typ └────┘└────────────────┘┴ └──┘ ┴└───┘└─────────────┘└┘
doc └────┘ ┴ └──┘ ┴└───┘ └┘
txt └────┘ ┴ └──┘ ┴└───┘ └┘
par └────┘ ┴ └──┘ ┴└───┘ └┘
pid ┴ ┴ └──┘ └────┘ ┴┴
st ──────────────────────────────────────┘└───────────────────┘└┘└─
778 end,
st ────┘
779 trimmed := begin
st └─────
780 letI := null_measurable μ,
id └─────────────┘ ┴
src └──────┘└─────────────┘┴
typ └──────┘└─────────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴└─┘ ┴
st ────────────────────────────┘└─
781 refine le_antisymm (λ s, _) (outer_measure.trim_ge _),
id └─────────┘ └───────────────────┘
src └─────┘└─────────┘┴ └─────┘ └───────────────────┘└─┘
typ └─────┘└─────────┘┴ └─────┘ └───────────────────┘└─┘
doc └─────┘ ┴ └─────┘ └─┘
txt └─────┘ ┴ └─────┘ └─┘
par └─────┘ ┴ └─────┘ └─┘
pid ┴ ┴ └─────┘ └─┘
st ────────────────────────────────────────────────────────┘└─
782 rw outer_measure.trim_eq_infi,
id └────────────────────────┘
src └─┘└────────────────────────┘
typ └─┘└────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────────┘└─
783 dsimp, clear _inst,
src └───┘ └─────────┘
typ └───┘ └─────────┘
doc └───┘ └─────────┘
txt └───┘ └─────────┘
par └───┘ └─────────┘
pid └────┘
st ────────┘└───────────┘└─
784 rw measure_eq_infi s,
id └─────────────┘ ┴
src └─┘└─────────────┘┴
typ └─┘└─────────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───────────────────────┘└─
785 exact infi_le_infi (λ t, infi_le_infi $ λ st,
id └──────────┘
src └────┘ ┴ └──┘└──────────┘┴ ┴ └────
typ └────┘ ┴ └──┘└──────────┘┴ ┴ └────
doc └────┘ ┴ └──┘ ┴ ┴ └────
txt └────┘ ┴ └──┘ ┴ ┴ └────
par └────┘ ┴ └──┘ ┴ ┴ └────
pid ┴ ┴ └──┘ ┴ ┴ └────
st ──────────────────────────────────────────────────
786 infi_le_infi2 $ λ ht, ⟨ht.is_null_measurable _, le_refl _⟩)
id └───────────┘ └─────────────────┘ └─────┘
src ─────┘└───────────┘┴ ┴ └───┘ └─────────────────┘└──┘└─────┘└────
typ ─────┘└───────────┘┴ ┴ └───┘ └─────────────────┘└──┘└─────┘└────
doc ─────┘ ┴ ┴ └───┘ └──┘ └────
txt ─────┘ ┴ ┴ └───┘ └──┘ └────
par ─────┘ ┴ ┴ └───┘ └──┘ └────
pid ─────┘ ┴ ┴ └───┘ └──┘ └──┘└
st ──────────────────────────────────────────────────────────────────
787 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
788
789 instance completion.is_complete {α : Type u} [measurable_space α] (μ : measure α) :
id └──────────────┘ ┴ └─────┘ ┴
src └──────────────┘ └─────┘
typ └──────────────┘ ┴ └─────┘ ┴
790 (completion μ).is_complete :=
id └────────┘ ┴ └─────────┘
src └────────┘ └─────────┘
typ └────────┘ ┴ └─────────┘
791 λ z hz, null_is_null_measurable hz
id ┴ └┘ └─────────────────────┘ └┘
src └─────────────────────┘
typ ┴ └┘ └─────────────────────┘ └┘
792
793 end is_complete
794
795 namespace measure_theory
796
797 section prio
798 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
799 /-- A measure space is a measurable space equipped with a
800 measure, referred to as `volume`. -/
801 class measure_space (α : Type*) extends measurable_space α :=
id └───┘ └──────────────┘ ┴
src └──────────────┘
typ └───┘ └──────────────┘ ┴
802 (μ {} : measure α)
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
803 end prio
804
805 section measure_space
806 variables {α : Type*} [measure_space α] {s₁ s₂ : set α}
id ┴ └───────────┘ └─┘
src └───────────┘ └─┘
typ ┴ └───────────┘ └─┘
doc └───────────┘
807 open measure_space
808
809 def volume : set α → ennreal := @μ α _
id └─┘ ┴ └─────┘ ┴ ┴
src └─┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ ┴
doc └─────┘
810
811 @[simp] lemma volume_empty : volume (∅ : set α) = 0 := μ.empty
id └────┘ ┴ └─┘ ┴ ┴ ┴└────┘
src └────┘ ┴ └─┘ ┴ ┴└────┘
typ └────┘ ┴ └─┘ ┴ ┴ ┴└────┘
doc └──┘
812
813 lemma volume_mono : s₁ ⊆ s₂ → volume s₁ ≤ volume s₂ := measure_mono
id └┘ ┴ └┘ └────┘ └┘ ┴ └────┘ └┘ └──────────┘
src ┴ └────┘ ┴ └────┘ └──────────┘
typ └┘ ┴ └┘ └────┘ └┘ ┴ └────┘ └┘ └──────────┘
814
815 lemma volume_mono_null : s₁ ⊆ s₂ → volume s₂ = 0 → volume s₁ = 0 :=
id └┘ ┴ └┘ └────┘ └┘ ┴ └────┘ └┘ ┴
src ┴ └────┘ ┴ └────┘ ┴
typ └┘ ┴ └┘ └────┘ └┘ ┴ └────┘ └┘ ┴
816 measure_mono_null
id └───────────────┘
src └───────────────┘
typ └───────────────┘
817
818 theorem volume_Union_le {β} [encodable β] :
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └───────┘
819 ∀ (s : β → set α), volume (⋃i, s i) ≤ (∑i, volume (s i)) :=
id ┴ ┴ └─┘ ┴ └────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └────┘ ┴ ┴
src └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘
typ ┴ ┴ └─┘ ┴ └────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └────┘ ┴ ┴
doc ┴ ┴ ┴ ┴
820 measure_Union_le
id └──────────────┘
src └──────────────┘
typ └──────────────┘
821
822 lemma volume_Union_null {β} [encodable β] {s : β → set α} :
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
823 (∀ i, volume (s i) = 0) → volume (⋃i, s i) = 0 :=
id ┴ └────┘ ┴ ┴ ┴ └────┘ ┴┴┴ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴
824 measure_Union_null
id └────────────────┘
src └────────────────┘
typ └────────────────┘
825
826 theorem volume_union_le : ∀ (s₁ s₂ : set α), volume (s₁ ∪ s₂) ≤ volume s₁ + volume s₂ :=
id └─┘ ┴ └────┘ └┘ ┴ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘
src └─┘ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ └─┘ ┴ └────┘ └┘ ┴ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘
827 measure_union_le
id └──────────────┘
src └──────────────┘
typ └──────────────┘
828
829 lemma volume_union_null : volume s₁ = 0 → volume s₂ = 0 → volume (s₁ ∪ s₂) = 0 :=
id └────┘ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘ ┴ └┘ ┴
src └────┘ ┴ └────┘ ┴ └────┘ ┴ ┴
typ └────┘ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘ ┴ └┘ ┴
830 measure_union_null
id └────────────────┘
src └────────────────┘
typ └────────────────┘
831
832 lemma volume_Union {β} [encodable β] {f : β → set α} :
id └───────┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
833 pairwise (disjoint on f) → (∀i, is_measurable (f i)) →
id └──────┘ └──────┘ └┘ ┴ ┴ └───────────┘ ┴ ┴
src └──────┘ └──────┘ └┘ └───────────┘
typ └──────┘ └──────┘ └┘ ┴ ┴ └───────────┘ ┴ ┴
doc └──────┘ └──────┘ └───────────┘
834 volume (⋃i, f i) = (∑i, volume (f i)) :=
id └────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └────┘ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ └────┘
typ └────┘ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └────┘ ┴ ┴
doc ┴ ┴ ┴ ┴
835 measure_Union
id └───────────┘
src └───────────┘
typ └───────────┘
836
837 lemma volume_union : disjoint s₁ s₂ → is_measurable s₁ → is_measurable s₂ →
id └──────┘ └┘ └┘ └───────────┘ └┘ └───────────┘ └┘
src └──────┘ └───────────┘ └───────────┘
typ └──────┘ └┘ └┘ └───────────┘ └┘ └───────────┘ └┘
doc └──────┘ └───────────┘ └───────────┘
838 volume (s₁ ∪ s₂) = volume s₁ + volume s₂ :=
id └────┘ └┘ ┴ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘
src └────┘ ┴ ┴ └────┘ ┴ └────┘
typ └────┘ └┘ ┴ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘
839 measure_union
id └───────────┘
src └───────────┘
typ └───────────┘
840
841 lemma volume_bUnion {β} {s : set β} {f : β → set α} : countable s →
id └─┘ ┴ ┴ └─┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ └─┘ ┴ ┴ └─┘ ┴ └───────┘ ┴
doc └───────┘
842 pairwise_on s (disjoint on f) → (∀b∈s, is_measurable (f b)) →
id └─────────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └─────────┘ └──────┘ └┘ └───────────┘
typ └─────────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────┘ └──────┘ └───────────┘
843 volume (⋃b∈s, f b) = ∑p:s, volume (f p.1) :=
id └────┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴┴
src └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
typ └────┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴┴
doc ┴ ┴ ┴ ┴
844 measure_bUnion
id └────────────┘
src └────────────┘
typ └────────────┘
845
846 lemma volume_sUnion {S : set (set α)} : countable S →
id └─┘ └─┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ └─┘ └─┘ ┴ └───────┘ ┴
doc └───────┘
847 pairwise_on S disjoint → (∀s∈S, is_measurable s) →
id └─────────┘ ┴ └──────┘ ┴ ┴ └───────────┘ ┴
src └─────────┘ └──────┘ └───────────┘
typ └─────────┘ ┴ └──────┘ ┴ ┴ └───────────┘ ┴
doc └─────────┘ └──────┘ └───────────┘
848 volume (⋃₀ S) = ∑s:S, volume s.1 :=
id └────┘ └┘ ┴ ┴ ┴ ┴┴ └────┘ ┴┴
src └────┘ └┘ ┴ ┴ ┴ └────┘ ┴
typ └────┘ └┘ ┴ ┴ ┴ ┴┴ └────┘ ┴┴
doc ┴ ┴
849 measure_sUnion
id └────────────┘
src └────────────┘
typ └────────────┘
850
851 lemma volume_bUnion_finset {β} {s : finset β} {f : β → set α}
id └────┘ ┴ ┴ └─┘ ┴
src └────┘ └─┘
typ └────┘ ┴ ┴ └─┘ ┴
doc └────┘
852 (hd : pairwise_on ↑s (disjoint on f)) (hm : ∀b∈s, is_measurable (f b)) :
id └─────────┘ ┴┴ └──────┘ └┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └─────────┘ ┴ └──────┘ └┘ └───────────┘
typ └─────────┘ ┴┴ └──────┘ └┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └─────────┘ └──────┘ └───────────┘
853 volume (⋃b∈s, f b) = s.sum (λp, volume (f p)) :=
id └────┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
src └────┘ ┴ ┴ ┴ └──┘ └────┘
typ └────┘ ┴┴ ┴┴ ┴ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
doc ┴ ┴
854 show volume (⋃b∈(↑s : set β), f b) = s.sum (λp, volume (f p)),
id └────┘ ┴┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
src └────┘ ┴ ┴ └─┘ ┴ ┴ └──┘ └────┘
typ └────┘ ┴┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
doc ┴ ┴
855 begin
st └─────
856 rw [volume_bUnion (countable_finite (finset.finite_to_set s)) hd hm, tsum_eq_sum],
id └───────────┘ └──────────────┘ └──────────────────┘ ┴ └┘ └┘ └─────────┘
src └──┘└───────────┘┴ └──────────────┘┴ └──────────────────┘┴ └─┘ ┴ └┘└─────────┘┴
typ └──┘└───────────┘┴ └──────────────┘┴ └──────────────────┘┴┴└─┘└┘┴└┘└┘└─────────┘┴
doc └──┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴
txt └──┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴
par └──┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴
pid └┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────────────┘└───────────┘└──
857 { show s.attach.sum (λb:(↑s : set β), volume (f b)) = s.sum (λb, volume (f b)),
id └──────────┘ ┴┴ └─┘ ┴ ┴ └───┘ └────┘ ┴
src └───┘└──────────┘┴ └┘ ┴ └─┘└─┘┴ └─┘ ┴ ┴ └─┘┴┴└───┘┴ └─┘└────┘┴ ┴ └┘
typ └───┘└──────────┘┴ └┘┴┴ └─┘└─┘┴┴└─┘ ┴ ┴ └─┘┴┴└───┘┴ └─┘└────┘┴ ┴┴ └┘
doc └───┘└──────────┘┴ └┘ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt └───┘ ┴ └┘ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └───┘ ┴ └┘ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └───┘ ┴ └┘ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ───┘└──────────────────────────────────────────────────────────────────────────┘└─
858 exact @finset.sum_attach _ _ s _ (λb, volume (f b)) },
id └───────────────┘ ┴ └────┘ ┴
src └────┘ └───────────────┘└───┘ └─┘ └─┘└────┘┴ ┴ └─┘
typ └────┘ └───────────────┘└───┘┴└─┘ └─┘└────┘┴ ┴┴ └─┘
doc └────┘ └───┘ └─┘ └─┘ ┴ ┴ └─┘
txt └────┘ └───┘ └─┘ └─┘ ┴ ┴ └─┘
par └────┘ └───┘ └─┘ └─┘ ┴ ┴ └─┘
pid ┴ └───┘ └─┘ └─┘ ┴ ┴ └┘┴
st ───────────────────────────────────────────────────────┘└┘└
859 simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
860 end
st └─┘
861
862 lemma volume_diff : s₂ ⊆ s₁ → is_measurable s₁ → is_measurable s₂ →
id └┘ ┴ └┘ └───────────┘ └┘ └───────────┘ └┘
src ┴ └───────────┘ └───────────┘
typ └┘ ┴ └┘ └───────────┘ └┘ └───────────┘ └┘
doc └───────────┘ └───────────┘
863 volume s₂ < ⊤ → volume (s₁ \ s₂) = volume s₁ - volume s₂ :=
id └────┘ └┘ ┴ ┴ └────┘ └┘ ┴ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘
src └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ └────┘ └┘ ┴ ┴ └────┘ └┘ ┴ └┘ ┴ └────┘ └┘ ┴ └────┘ └┘
864 measure_diff
id └──────────┘
src └──────────┘
typ └──────────┘
865
866 /-- `∀ₘ a:α, p a` states that the property `p` is almost everywhere true in the measure space
867 associated with `α`. This means that the measure of the complementary of `p` is `0`.
868
869 In a probability measure, the measure of `p` is `1`, when `p` is measurable.
870 -/
871 def all_ae (p : α → Prop) : Prop :=
id ┴
typ ┴
872 ∀ᶠ a in μ.a_e, p a
id └┘ ┴ └┘ ┴└──┘┴ ┴ ┴
src └┘ └┘ ┴└──┘┴
typ └┘ ┴ └┘ ┴└──┘┴ ┴ ┴
doc └┘ └┘ └──┘┴
873
874 notation `∀ₘ` binders `, ` r:(scoped P, all_ae P) := r
id └────┘
src └────┘
typ └────┘
doc └────┘
875
876 lemma all_ae_congr {p q : α → Prop} (h : ∀ₘ a, p a ↔ q a) : (∀ₘ a, p a) ↔ (∀ₘ a, q a) :=
id ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
doc └┘ ┴ └┘ ┴ └┘ ┴
877 iff.intro
id └───────┘
src └───────┘
typ └───────┘
878 (assume h', by filter_upwards [h, h'] assume a hpq hp, hpq.1 hp)
id └┘
src └──────────────┘ └┘ └┘ └─────────┘ └─┘
typ └┘ └──────────────┘ └┘ └┘ └─────────┘ └─┘
doc └──────────────┘ └┘ └┘ └─────────┘ └─┘
txt └──────────────┘ └┘ └┘ └─────────┘ └─┘
par └──────────────┘ └┘ └┘ └─────────┘ └─┘
pid └┘ └┘ ┴┴ └─────────┘ └─┘
st └───────────────────────────────────────────────┘
879 (assume h', by filter_upwards [h, h'] assume a hpq hq, hpq.2 hq)
id └┘
src └──────────────┘ └┘ └┘ └─────────┘ └─┘
typ └┘ └──────────────┘ └┘ └┘ └─────────┘ └─┘
doc └──────────────┘ └┘ └┘ └─────────┘ └─┘
txt └──────────────┘ └┘ └┘ └─────────┘ └─┘
par └──────────────┘ └┘ └┘ └─────────┘ └─┘
pid └┘ └┘ ┴┴ └─────────┘ └─┘
st └───────────────────────────────────────────────┘
880
881 lemma all_ae_iff {p : α → Prop} : (∀ₘ a, p a) ↔ volume { a | ¬ p a } = 0 := iff.rfl
id ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └┘ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘
typ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └┘ ┴
882
883 lemma all_ae_of_all {p : α → Prop} : (∀a, p a) → ∀ₘ a, p a := univ_mem_sets'
id ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ └────────────┘
src └┘ ┴ └────────────┘
typ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ └────────────┘
doc └┘ ┴
884
885 lemma all_ae_all_iff {ι : Type*} [encodable ι] {p : α → ι → Prop} :
id └───────┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴
doc └───────┘
886 (∀ₘ a, ∀i, p a i) ↔ (∀i, ∀ₘ a, p a i) :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴
src └┘ ┴ ┴ └┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └┘ ┴ └┘ ┴
887 begin
st └─────
888 refine iff.intro (assume h i, _) (assume h, _),
id └───────┘
src └─────┘└───────┘┴ └───────┘ └────┘
typ └─────┘└───────┘┴ └───────┘ └────┘
doc └─────┘ ┴ └───────┘ └────┘
txt └─────┘ ┴ └───────┘ └────┘
par └─────┘ ┴ └───────┘ └────┘
pid ┴ ┴ └───────┘ └────┘
st ───────────────────────────────────────────────┘└─
889 { filter_upwards [h] assume a ha, ha i },
id ┴
src └──────────────┘ └┘ └─────┘ ┴ ┴
typ └──────────────┘ └┘ └─────┘ ┴┴┴
doc └──────────────┘ └┘ └─────┘ ┴ ┴
txt └──────────────┘ └┘ └─────┘ ┴ ┴
par └──────────────┘ └┘ └─────┘ ┴ ┴
pid └┘ ┴┴ └─────┘ ┴ ┴
st ───┘└───────────────────────────────────┘└┘└
890 { have h := measure_Union_null h,
id └────────────────┘ ┴
src └────────┘└────────────────┘┴
typ └────────┘└────────────────┘┴┴
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid └────┘┴└─┘ ┴
st ─────────────────────────────────┘└─
891 rw [← compl_Inter] at h,
id └─────────┘
src └────┘└─────────┘└────┘
typ └────┘└─────────┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid └──┘ ┴└───┘
st ────────────────────┘┴└───┘└─
892 filter_upwards [h] assume a, mem_Inter.1 }
id └───────┘
src └──────────────┘ └┘ └──┘└───────┘└─┘
typ └──────────────┘ └┘ └──┘└───────┘└─┘
doc └──────────────┘ └┘ └──┘ └─┘
txt └──────────────┘ └┘ └──┘ └─┘
par └──────────────┘ └┘ └──┘ └─┘
pid └┘ ┴┴ └──┘ └─┘
st ────────────────────────────────────────────┘└─
893 end
st ──┘
894
895 variables {β : Type*}
896
897 lemma all_ae_eq_refl (f : α → β) : ∀ₘ a, f a = f a :=
id ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴
898 by { filter_upwards [], assume a, apply eq.refl }
id └─────┘
src └───────────────┘ └──────┘ └────┘└─────┘┴
typ └───────────────┘ └──────┘ └────┘└─────┘┴
doc └───────────────┘ └──────┘ └────┘ ┴
txt └───────────────┘ └──────┘ └────┘ ┴
par └───────────────┘ └──────┘ └────┘ ┴
pid └─┘ └──────┘ ┴ ┴
st └──────────────────┘└────────┘└──────────────┘└┘
899
900 lemma all_ae_eq_symm {f g : α → β} : (∀ₘ a, f a = g a) → (∀ₘ a, g a = f a) :=
id ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴ └┘ ┴
901 by { assume h, filter_upwards [h], assume a, apply eq.symm }
id └─────┘
src └──────┘ └──────────────┘ ┴ └──────┘ └────┘└─────┘┴
typ └──────┘ └──────────────┘ ┴ └──────┘ └────┘└─────┘┴
doc └──────┘ └──────────────┘ ┴ └──────┘ └────┘ ┴
txt └──────┘ └──────────────┘ ┴ └──────┘ └────┘ ┴
par └──────┘ └──────────────┘ ┴ └──────┘ └────┘ ┴
pid └──────┘ └┘ ┴ └──────┘ ┴ ┴
st └─────────┘└──────────────────┘└────────┘└──────────────┘└┘
902
903 lemma all_ae_eq_trans {f g h: α → β} (h₁ : ∀ₘ a, f a = g a) (h₂ : ∀ₘ a, g a = h a) :
id ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴ └┘ ┴
904 ∀ₘ a, f a = h a :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴
905 by { filter_upwards [h₁, h₂], intro a, exact eq.trans }
id └──────┘
src └──────────────┘ └┘ ┴ └─────┘ └────┘└──────┘┴
typ └──────────────┘ └┘ ┴ └─────┘ └────┘└──────┘┴
doc └──────────────┘ └┘ ┴ └─────┘ └────┘ ┴
txt └──────────────┘ └┘ ┴ └─────┘ └────┘ ┴
par └──────────────┘ └┘ ┴ └─────┘ └────┘ ┴
pid └┘ └┘ ┴ └┘ ┴ ┴
st └────────────────────────┘└───────┘└───────────────┘└┘
906
907 end measure_space
908
909 end measure_theory